[TYPES/announce] Postdoc: Program Analysis with Separation Logic

[Peter O'Hearn]

Postdoc Position in Program Analysis with Separation Logic
Dept of Computer Science, Queen Mary, University of London

A full time Research Assistant position is available for 22 months  
from 1 October 2007 on the EPSRC-funded Smallfoot project. The aim of  
the project is to develop an automatic verification tool for pointer  
usage in C programs using separation logic. The project builds on an  
earlier Smallfoot prototype, and also the Space Invader program  
analysis. You should have experience in program analysis, as  
evidenced by your publication record, and relevant knowledge of  
separation logic and shape analysis. The project calls for both  
theoretical development of new ideas in program analysis and  
verification, and practical development of the tool.

Smallfoot is a jointly-funded project between Peter O'Hearn at Queen  
Mary and Cristiano Calcagno and Philippa Gardner at Imperial College.  
The advertised position is at Queen Mary, where the team also  
includes Dino Distefano and Hongseok Yang (originators of Space  
Invader). The position has become open as a result of Distefano, the  
previous RA, obtaining a 5-year research fellowship from the UK Royal  
Academy of Engineering. James Brotherston is the project's RA at  
Imperial.

The London teams maintain a close working relationship with Josh  
Berdine and Byron Cook from Microsoft Cambridge. Early work on the  
project has resulted in verification of data structure usage for  
several routines from a firewire device driver for Windows, as well  
as the discovery of previously-unknown heap-manipulation bugs.

See
http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html
to get an idea of our recent work.

If you have any questions on the position contact Peter O'Hearn  
(ohearn at dcs.qmul.ac.uk).
Application packs with forms and departmental information can be  
found on
    http://www.dcs.qmul.ac.uk/staff/recruit/QMApplicationFormBlue1.pdf
or please visit
    http://www.hr.qmul.ac.uk/vacancies

Completed application forms with full CV and contact details for  
three independent references should be returned either by e-mail to  
ohearn at dcs.qmul.ac.uk or by surface mail to

Professor Peter O'Hearn
Department of Computer Science
Queen Mary, University of London
Mile End Road, London, E1 4NS, UK.

The closing date for applications is 15 July 2007.