[Prev][Next][Index][Thread]

Postdoc Position in Separation Logic

Research Assistant in Separation Logic
Department of Computer Science
Queen Mary, University of London
Start Date: 1 Jan, 2004
Duration: 3 years

A Research Assistant position is is available on the EPSRC-funded Applications
of Local Reasoning project. This is a project to apply the recent
formalism of separation logic to problems in program analysis and
mechanical verification. Automatic analysis and lightweight assertional 
techniques will be developed to ensure structural integrity properties of 
pointer-based data structures. Machine-assisted proof will be used to 
tackle crucial pieces of the fundamental code that forms the basis of 
our computing infrastructure, such as code found in language 
runtimes, operating system kernels, or internet routers.

You will work with Prof Peter O'Hearn and others, in an active group
of researchers on Separation Logic in the London area.
You should have, or be expecting, a PhD
in Computer Science, or have other relevant experience.

It is early days in the application of separation logic, and
there is considerable flexibility in both the choice of problems we will 
tackle and in the background expected of the candidate. 
Expertise in one of the following areas would be helpful:
  - Program analysis, abstract interpretation, and model checking;
  - Tactic-based Proof (e.g., HOL, Isabelle, Coq);
  - Automatic Theorem Proving, including decision procedures;
  - Program Logic; or
  - Type Systems.
Familiarity with Hoare logic, linear logic, bunched logic or separation logic 
would also be an asset.

The salary is on the RA1A Scale, 20579 to 29654 GBP (inclusive of London 
weighting) depending on age and experience.  The starting date
is 1 January 2004, or as soon as possible thereafter, and the project runs 
for three years.

If you have any questions on the position
contact Peter O'Hearn (ohearn@dcs.qmul.ac.uk).
More information, including background and project description, is on
  http://nick.dcs.qmul.ac.uk/~ohearn/Adverts/RA/

Application packs with forms and departmental information can
be found on
  http://www.dcs.qmul.ac.uk/public/recruitment/

Completed application forms with full CV and contact details for
three independent references should be returned either by e-mail to
  ohearn@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 1 November, 2003.