[TYPES/announce] research position at Imperial, Smallfoot checker

[Cristiano Calcagno]

Philippa Gardner and I have a three-year postdoctoral research position
available at Imperial, to build a static assertion checker for C based
on separation logic. This is a joint project with Peter O'Hearn at Queen
Mary, comprising one PhD student and one RA at each site.

The details are given below. The deadline for application is 28th July
2006. Please send informal enquiries to me.

I'd be grateful if you could forward this email to candidates you think
might be suitable.

Best wishes,

Cristiano Calcagno

------------------------

Research Assistant/Associate
Department of Computing, Imperial College London

Title: Smallfoot: Static Assertion Checking for C programs

Salary: £22,870 - £33,330 inclusive of London Allowance per annum

Deadline for Applications: 28th July 2006

A postdoctoral Research Fellowship is available in the Department of
Computing to work with Cristiano Calcagno and Philippa Gardner on an
EPSRC project joint with Peter O'Hearn at Queen Mary. This is a fixed
term post of 3 years starting on 1 October 2006 with some flexibility.
The aim of the project is to develop a static assertion checker for C
based on separation logic, and demonstrate it on systems code such as a
memory manager. See
http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot/ for
more details.

Applicants must hold, or being nearing completion of, a PhD in Computer
Science in a relevant subject. Preference will be given to applicants
with a proven record in software development or theoretical computer
science. Experience in one or more of the following is desirable: logic
(especially separation logic), verification, program analysis, model
checking.

Formal applications should be sent to the address at the end of this
message. Please send informal enquiries to

  Cristiano Calcagno, email: ccris at doc.ic.ac.uk


Background of the Project
-------------------------

Pointers have long been one of the dark corners of programming
languages. Tractable proof and analysis tools are lacking for all but
the most simple, shallow, properties of the program heap. A recent
theory, separation logic, has shed fresh light on this area, and has
generated considerable interest worldwide. It has lead to much simpler
by-hand specifications and program proofs than previous formalisms, and
it suggests, for the first time, the possibility of scalable analysis
methods for expressive heap properties. To date though, separation logic
remains mainly a theoretical advance; there are no tools based on
separation logic for any real programming languages.
We propose to develop a static assertion checker for C based on
separation logic. Separation logic works naturally with a low-level RAM
model, and thus appears to be well suited to code that must run close to
the hardware without an intermediate abstraction of the kind found in
the runtimes of high-level languages such as ML or Java. Much
fundamental code of this sort is written in the C programming language,
and is outside the effective range of current tools.
Our tool, Smallfoot, will accept precondition and postcondition
assertions written in separation logic, and programs will be checked
using a combination of symbolic execution and specialized proof
procedures. Abstract interpretation will be used to alleviate the need
to state invariants. We will check structural integrity properties of
programs -- such as that data structures are in consistent states, or
that resource boundaries are respected -- rather than full functional
correctness. In this way we hope to keep specifications simple, and to
achieve a high degree of automation. As it is aimed at low-level
programs, Smallfoot will be complementary to static assertion checkers
for higher-level languages such as the ESC tool for Java and the Spec#
tool for C#.
Success on the problems in this project could have a significant impact
on the use of logic to check properties of systems programs.


Application
-----------

Applications should include a College application form, which can be
obtained from http://www.imperial.ac.uk/employment/academicform.htm.
Applications should be on the correct form quoting Job Reference Number:
Smallfoot 06. Applications must include a full CV, stating the names and
addresses of three referees and should be sent to:

Nicola Rogers
Department of Computing,
Imperial College London,
South Kensington Campus,
London, SW7 2AZ

email: n.c.rogers at imperial.ac.uk