[TYPES/announce] Post-doctoral research associate in program verification

[Matthew Parkinson]

POST-DOCTORAL RESEARCH ASSOCIATE IN PROGRAM VERIFICATION

Computer Laboratory, University of Cambridge, UK

======

A full-time three year Research Associate position is available on an  
EPSRC-funded project "Modular verification of concurrent programs:  
Marrying Rely-Guarantee and Separation Logic".

The aim of the project is to develop tractable reasoning about  
concurrent algorithms. The project calls for both theoretical  
development of new ideas in program verification, and practical  
development of tool support for verification and analysis.

In particular, the project builds on our previous work on combining  
the rely/guarantee method with separation logic to provide modular  
verification of concurrent algorithms: see http://www.cl.cam.ac.uk/ 
~mjp41/RGSep.pdf

The successful candidate should have, or be close to finishing, a PhD  
in Computer Science, and should have a background in programming  
languages or theorem proving as shown by their publication record.  
Experience in program verification or analysis is highly desirable.  
Previous development experience with OCaml and Java would be beneficial.

Closing date: 19 October 2007. This post is intended to be filled as  
soon as practical after the closing date. However, a start date up  
until March 2008 can be negotiated.

Full details of the job are at: http://www.jobs.ac.uk/jobs/SI689/ 
Research_Associate/

Enquiries about the project should be addressed to Dr Matthew  
Parkinson (mjp41 at cl.cam.ac.uk)