Ph.D and Postdoc Positions available in Durham, UK

Ph.D and Postdoc Positions available in Durham, UK

[CRACIUN F.]

[-- Attachment #1: Type: text/plain, Size: 4229 bytes --]


************************************************************

* A 3.5year Ph.D Position and a Postdoc Position 

* available in the area of Program Analysis and Verification

* funded by the EPSRC project entitled "Inference Mechanisms 

* for a Separation and Numerical Domain"

* in Department Of Computer Science, Durham University, UK

************************************************************





Applications are invited for a Ph.D. student and a Postdoctoral Research Associate to work on an EPSRC funded project entitled "Inference Mechanisms for a Separation and Numerical Domain" in the group led by Dr. Shengchao Qin in the Department of Computer Science. The aim of the project is to develop advanced static analysis techniques based on separation logic for automated verification of memory safety as well as functional correctness of substantial heap-manipulating imperative programs. The key objective is to develop advanced inference/abstraction mechanisms in the combined separation and numerical domain with user-defined inductive predicates, so that loop invariants and method pre/post-conditions can be automatically synthesised, where possible.





About the Ph.D Position:

=========================



Prospective Ph.D candidates must have (or expect to have) a good honours (or equivalent) degree in Computer Science or other relevant subjects. The studentship requires good background knowledge in most of the following areas: logic and discrete mathematics related to computer science, computer-aided verification, compilers, and program analysis. Strong programming skills will also be essential for the studentship.



This fully funded studentship provides a tax-free living allowance at the standard EPSRC rate (GBP 13,290 p.a. for 09/10) and student tuition fees at the UK/EU student rate (non-EU students will require supplementary funding). The successful candidate is expected to start on 1st September 2009.



Closing date (the Ph.D Position): 15 May 2009



Applications (such as CV, references, a transcript and a statement of research interests) should be sent to Dr Shengchao Qin, Computer Science Department, Durham University, Science Labs, South Road, Durham, DH1 3LE, United Kingdom. Applicants are also required to register their interest of pursuing a Ph.D in Durham at https://bannerss.dur.ac.uk/blive_ssb/bwskalog.P_DispLoginNon





About the Postdoc Position:

===========================



The successful applicant should have received (or expect to receive) a Ph.D in Computer Science or a closely related subject.  Suitable candidates should be able to demonstrate research skills or potential at an international level in the field of program analysis and computer-aided verification.



Key responsibilities: the Postdoctoral Research Associate(PDRA) is expected to conduct research in program analysis and verification using separation logic.  Working closely with the team leader, the PDRA is expected to develop advanced inference/abstraction mechanisms in an abstract domain combined with separation and numerical information and in the presence of user-specified inductive predicates and lemmas. More specifically, the PDRA is expected to make significant contributions in (1) automatic inference/analysis  of loop invariants and method pre/post-specifications in the combined domain, (2) the construction of an analysis/verification tool and the integration of the developed tool with the verification tool HIP/SLEEK developed in National University of Singapore, and (3) the application of the tool to verify memory safety of substantial system software such as the Linux distribution.  The RA is expected to write and publish research papers in good quality conferences and journals every year. 



Closing date (the Postdoc postioin): 31 May 2009



Details about this position including the application procedure can be found at

https://jobs.dur.ac.uk/jobdtls.asp?Session_in=&Uid=&vref=3164





More project information can be obtained by contacting Dr Shengchao Qin at shengchao.qin@durham.ac.uk, or by visiting http://www.dur.ac.uk/shengchao.qin

















[-- Attachment #2: Type: text/html, Size: 5227 bytes --]

TASE 2009 - Call for Participation

[CRACIUN F.]

[-- Attachment #1: Type: text/plain, Size: 7836 bytes --]


        TASE 2009 - CALL FOR PARTICIPATION

**********************************************************
*    3rd IEEE International Symposium on
* Theoretical Aspects of Software Engineering
*             (TASE 2009)
*     29-31 July 2009, Tianjin, China
*    http://www.dur.ac.uk/ieee.tase2009
*
* Early Registration Deadline : 18 June 2009
* For more information email: IEEE.TASE2009@durham.ac.uk
***********************=**********************************


TASE 2009 Invited Speakers
==========================

Kim G. Larsen, Aalborg University, Denmark

Zhong Shao, Yale University, USA
 
Jin-Song Dong, National University of Singapore

 
 
TASE 2009 Programme
====================

Day 1: 29 July 2009
-------------------

Invited Talk:

Verification and Performance Analysis of Embedded Systems
Kim G. Larsen (Aalborg University)

Session 1 : Real-Time and Embedded Systems

Improving Responsiveness of Hard Real-Time Embedded Systems
Hugh Anderson (Wellington Institute of Technology) and Siau-Cheng KHOO (National University of Singapore)  

Environmental Simulation of Real-Time Systems with Nested Interrupts
Guoqiang Li (Shanghai Jiao Tong University), Shoji Yuen (Nagoya University) and Masakazu Adachi (Toyota Central R&D Labs. INC.). 

Semantics for Communicating Actors with Interdependent Real-Time Deadlines
Istv¨¢n Knoll (Aalborg University), Anders P. Ravn (Aalborg University) and Arne Skou (Aalborg University). 

An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems
Zhenhua Duan (Xidian University) and Yan Xiao (Xidian University). 

Session 2 : Semantics

State Visibility and Communication in Unifying Theories of Programming
Andrew Butterfield (Trinity College Dublin), Pawel Gancarski (Trinity College Dublin) and Jim Woodcock (University of York). 

Semantics of Metamodels in UML
Lijun Shan (National University of Defence Technology) and Hong Zhu (Oxford Brookes University). 

Refinement Algebra with Explicit Probabilism
Tahiry Rabehaja (UNU/IIST) and Jeffrey Sanders (UNU/IIST). 

Session 3 : Model Checking

Environment Abstraction with State Clustering and Parameter Truncating
Hong Pan (Institute of Software, Chinese Academy of Sciences), Yi Lv (Institute of Software, Chinese Academy of Sciences)  and Huimin Lin (Institute of Software, Chinese Academy of Sciences). 

Verification of Population Ring Protocols in PAT
Yang Liu (National University of Singapore), Jun Pang (University of Luxembourg), Jun Sun (National University of Singapore) and Jianhua Zhao (Nanjing University). 

Bounded Model Checking of ACTL Formulae
Wei Chen (Institute of Software, Chinese Academy of Sciences) and Wenhui Zhang (Institute of Software, Chinese Academy of Sciences). 

Day 2, 30 July 2009
-------------------

Invited Talk:

Modular Development of Certified System Software
Zhong Shao (Yale University)  

Session 4: Specification and Security

Coarse Grained Retrenchment and the Mondex Denial of Service Attacks
Richard Banach (Manchester University). 

Specifying and Enforcing Constraints of Artifact Life Cycles
Xiangpeng Zhao (Peking University), Jianwen Su (University of California at Santa Barbara), Hongli Yang (Beijing University of Technology) and Zongyan Qiu (Peking University). 

Consistency Checking for LSC Specifications
Hai-Feng Guo (University of Nebraska at Omaha), Wen Zheng (University of Nebraska at Omaha) and Mahadevan Subramaniam (University of Nebraska at Omaha). 

Integrating Specification and Programs for System Modeling and Verification
Jun Sun (National University of Singapore), Yang Liu (National University of Singapore), Jin Song Dong (National University of Singapore) and Chunqing Chen (National University of Singapore). 

Session 5 : Software Testing I

A Framework and  Language Support for Automatic Dynamic Testing of Workflow Management Systems
Gwan-Hwan Hwang (National Taiwan Normal University), Che-Sheng Lin (National Taiwan Normal University), Li-Te Tsao (National Taiwan Normal University), Kuei-Huan Chen (National Taiwan Normal University) and Yan-You Li (National Taiwan Normal University). 

Fault-based Test Case Generation for Component Connectors
Bernhard Aichernig (Graz University of Technology), Farhad Arbab (CWI), Lacramioara Astefanoaei (CWI), Frank de Boer (CWI), Meng Sun (CWI) and Jan Rutten (CWI). 

Test Data Generation for Derived Types in C Program
Zheng Wang (East China Normal University), Xiao Yu (East China Normal University), Tao Sun (East China Normal University), Geguang Pu (East China Normal University) and Zuohua Ding (Zhejiang Sci-Tech University). 

Session 6 : Software Models

Program Repair as Sound Optimization of Broken Programs 
Bernd Fischer (University of Southampton), Ando Saabas (Tallinn University of Technology) and Tarmo Uustalu (Tallinn University of Technology). 

Modeling Web Applications and Generating Tests: A Combination and Interactions-guided Approach 
Bo Song (Shanghai University) and Huaikou Miao (Shanghai University). 

Merging of Use Case Models: Semantic Foundations  
Stephen Barrett (Concordia University), Daniel Sinnig (Concordia University), Patrice Chalin (Concordia University) and Greg Butler (Concordia University). 

Day 3, 31 July 2009
-------------------

Invited Tutorial:

Towards Expressive Specification and Efficient Model Checking
Jin Song Dong (National University of Singapore)

Session 7 : Verification

Verifying Semistructured Data Normalization using SWRL
Yuan Fang Li (University of Queensland), Jing Sun (University of Auckland), Gillian Dobbie (University of Auckland), Scott Uk-Jin Lee (University of Auckland)  and Hai H. Wang (Aston University). 

Verifying Self-stabilizing Population Protocols with Coq
Yuxin Deng (Shanghai Jiao Tong University) and Jean-fran?ois Monin (Universit¨¦ de Grenoble 1).

The Logical Approach to Low-level Stack Reasoning
Xinyu Jiang (University of Science and Technology of China), Yu Guo (University of Science and Technology of China) and Yiyun Chen (University of Science and Technology of China). 

Constructing Program Invariants via Solving QBF
Shikun Chen (National University of Defence Technology), Zhoujun Li (Beihang University) and Mengjun Li (National University of Defence Technology). 

Session 8 : Concurrency 

Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation
Moritz Martens (University of Mannheim) and Mila Majster-Cederbaum (University of Mannheim). 

Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
Ming Fu (University of Science and Technology of China), Yu Zhang (University of Science and Technology of China) and Yong Li (University of Science and Technology of China). 

Algorithms for Computing Weak Bisimulation Equivalence
Weisong Li (Institute of Software, Chinese Academy of Sciences). 

Session 9 : Software Testing II

Interpreting a Successful Testing Process: Risk and Actual Coverage
Marielle Stoelinga (University of Twente) and Mark Timmer (University of Twente). 

Automated Test Case Generation based on Coverage Analysis
Tim A. Majchrzak (University of Muenster) and Herbert Kuchen (University of Muenster). 

Exploring Topological Structure of Boolean Expressions for Test Data Selection
Lian Yu (Peking University), Wei Zhao (IBM China Research Lab), Xiangdong Fan (Peking University) and Jun Zhu (IBM China Research Lab). 

On Testing 1-Safe Petri Nets
Guy-Vincent Jourdan (University of Ottawa) and Gregor von Bochmann (University of Ottawa). 


The programme also include two poster sessions, comprising
of 23 selected poster presentations. This list of posters can 
be found at http://www.dur.ac.uk/ieee.tase2009/
 


[-- Attachment #2: Type: text/html, Size: 9131 bytes --]

TASE 2009 - Call for Participation

[CRACIUN F.]

[-- Attachment #1: Type: text/plain, Size: 7851 bytes --]


 
        TASE 2009 - CALL FOR PARTICIPATION

**********************************************************
*    3rd IEEE International Symposium on
* Theoretical Aspects of Software Engineering
*             (TASE 2009)
*     29-31 July 2009, Tianjin, China
*    http://www.dur.ac.uk/ieee.tase2009
*
* Early Registration Deadline : 18 June 2009
* For more information email: IEEE.TASE2009@durham.ac.uk
***********************=**********************************


TASE 2009 Invited Speakers
==========================

Kim G. Larsen, Aalborg University, Denmark

Zhong Shao, Yale University, USA
 
Jin-Song Dong, National University of Singapore

 
 
TASE 2009 Programme
====================

Day 1: 29 July 2009
-------------------

Invited Talk:

Verification and Performance Analysis of Embedded Systems
Kim G. Larsen (Aalborg University)

Session 1 : Real-Time and Embedded Systems

Improving Responsiveness of Hard Real-Time Embedded Systems
Hugh Anderson (Wellington Institute of Technology) and Siau-Cheng KHOO (National University of Singapore)  

Environmental Simulation of Real-Time Systems with Nested Interrupts
Guoqiang Li (Shanghai Jiao Tong University), Shoji Yuen (Nagoya University) and Masakazu Adachi (Toyota Central R&D Labs. INC.). 

Semantics for Communicating Actors with Interdependent Real-Time Deadlines
Istv¨¢n Knoll (Aalborg University), Anders P. Ravn (Aalborg University) and Arne Skou (Aalborg University). 

An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems
Zhenhua Duan (Xidian University) and Yan Xiao (Xidian University). 

Session 2 : Semantics

State Visibility and Communication in Unifying Theories of Programming
Andrew Butterfield (Trinity College Dublin), Pawel Gancarski (Trinity College Dublin) and Jim Woodcock (University of York). 

Semantics of Metamodels in UML
Lijun Shan (National University of Defence Technology) and Hong Zhu (Oxford Brookes University). 

Refinement Algebra with Explicit Probabilism
Tahiry Rabehaja (UNU/IIST) and Jeffrey Sanders (UNU/IIST). 

Session 3 : Model Checking

Environment Abstraction with State Clustering and Parameter Truncating
Hong Pan (Institute of Software, Chinese Academy of Sciences), Yi Lv (Institute of Software, Chinese Academy of Sciences)  and Huimin Lin (Institute of Software, Chinese Academy of Sciences). 

Verification of Population Ring Protocols in PAT
Yang Liu (National University of Singapore), Jun Pang (University of Luxembourg), Jun Sun (National University of Singapore) and Jianhua Zhao (Nanjing University). 

Bounded Model Checking of ACTL Formulae
Wei Chen (Institute of Software, Chinese Academy of Sciences) and Wenhui Zhang (Institute of Software, Chinese Academy of Sciences). 

Day 2, 30 July 2009
-------------------

Invited Talk:

Modular Development of Certified System Software
Zhong Shao (Yale University)  

Session 4: Specification and Security

Coarse Grained Retrenchment and the Mondex Denial of Service Attacks
Richard Banach (Manchester University). 

Specifying and Enforcing Constraints of Artifact Life Cycles
Xiangpeng Zhao (Peking University), Jianwen Su (University of California at Santa Barbara), Hongli Yang (Beijing University of Technology) and Zongyan Qiu (Peking University). 

Consistency Checking for LSC Specifications
Hai-Feng Guo (University of Nebraska at Omaha), Wen Zheng (University of Nebraska at Omaha) and Mahadevan Subramaniam (University of Nebraska at Omaha). 

Integrating Specification and Programs for System Modeling and Verification
Jun Sun (National University of Singapore), Yang Liu (National University of Singapore), Jin Song Dong (National University of Singapore) and Chunqing Chen (National University of Singapore). 

Session 5 : Software Testing I

A Framework and  Language Support for Automatic Dynamic Testing of Workflow Management Systems
Gwan-Hwan Hwang (National Taiwan Normal University), Che-Sheng Lin (National Taiwan Normal University), Li-Te Tsao (National Taiwan Normal University), Kuei-Huan Chen (National Taiwan Normal University) and Yan-You Li (National Taiwan Normal University). 

Fault-based Test Case Generation for Component Connectors
Bernhard Aichernig (Graz University of Technology), Farhad Arbab (CWI), Lacramioara Astefanoaei (CWI), Frank de Boer (CWI), Meng Sun (CWI) and Jan Rutten (CWI). 

Test Data Generation for Derived Types in C Program
Zheng Wang (East China Normal University), Xiao Yu (East China Normal University), Tao Sun (East China Normal University), Geguang Pu (East China Normal University) and Zuohua Ding (Zhejiang Sci-Tech University). 

Session 6 : Software Models

Program Repair as Sound Optimization of Broken Programs 
Bernd Fischer (University of Southampton), Ando Saabas (Tallinn University of Technology) and Tarmo Uustalu (Tallinn University of Technology). 

Modeling Web Applications and Generating Tests: A Combination and Interactions-guided Approach 
Bo Song (Shanghai University) and Huaikou Miao (Shanghai University). 

Merging of Use Case Models: Semantic Foundations  
Stephen Barrett (Concordia University), Daniel Sinnig (Concordia University), Patrice Chalin (Concordia University) and Greg Butler (Concordia University). 

Day 3, 31 July 2009
-------------------

Invited Tutorial:

Towards Expressive Specification and Efficient Model Checking
Jin Song Dong (National University of Singapore)

Session 7 : Verification

Verifying Semistructured Data Normalization using SWRL
Yuan Fang Li (University of Queensland), Jing Sun (University of Auckland), Gillian Dobbie (University of Auckland), Scott Uk-Jin Lee (University of Auckland)  and Hai H. Wang (Aston University). 

Verifying Self-stabilizing Population Protocols with Coq
Yuxin Deng (Shanghai Jiao Tong University) and Jean-fran?ois Monin (Universit¨¦ de Grenoble 1).

The Logical Approach to Low-level Stack Reasoning
Xinyu Jiang (University of Science and Technology of China), Yu Guo (University of Science and Technology of China) and Yiyun Chen (University of Science and Technology of China). 

Constructing Program Invariants via Solving QBF
Shikun Chen (National University of Defence Technology), Zhoujun Li (Beihang University) and Mengjun Li (National University of Defence Technology). 

Session 8 : Concurrency 

Using Architectural Constraints for Deadlock-Freedom of Component Systems with Multiway Cooperation
Moritz Martens (University of Mannheim) and Mila Majster-Cederbaum (University of Mannheim). 

Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
Ming Fu (University of Science and Technology of China), Yu Zhang (University of Science and Technology of China) and Yong Li (University of Science and Technology of China). 

Algorithms for Computing Weak Bisimulation Equivalence
Weisong Li (Institute of Software, Chinese Academy of Sciences). 

Session 9 : Software Testing II

Interpreting a Successful Testing Process: Risk and Actual Coverage
Marielle Stoelinga (University of Twente) and Mark Timmer (University of Twente). 

Automated Test Case Generation based on Coverage Analysis
Tim A. Majchrzak (University of Muenster) and Herbert Kuchen (University of Muenster). 

Exploring Topological Structure of Boolean Expressions for Test Data Selection
Lian Yu (Peking University), Wei Zhao (IBM China Research Lab), Xiangdong Fan (Peking University) and Jun Zhu (IBM China Research Lab). 

On Testing 1-Safe Petri Nets
Guy-Vincent Jourdan (University of Ottawa) and Gregor von Bochmann (University of Ottawa). 


The programme also include two poster sessions, comprising
of 23 selected poster presentations. This list of posters can 
be found at http://www.dur.ac.uk/ieee.tase2009/
 








[-- Attachment #2: Type: text/html, Size: 9173 bytes --]