[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 ([EMAIL PROTECTED]). 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 [EMAIL PROTECTED] 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.