[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
[ Please forward to candidates who might be interested ]
---------------------------------------------------------------------------------------
Postdoctoral Research Fellowship
in
Formal Program Verification
-----------------------------------------------------------------------------------------
Department of Informatics, University of Sussex, Brighton, UK
Fixed term for 3 years, Full Time
Salary range: £28,290 to £33,780 per annum
Expected start date: at earliest, 1 October 2008
Project:
"From Reasoning Principles for Function Pointers To Logics for Self-
Configuring Programs"
Pointers are an important feature of programming languages used to
define dynamically growing and recursive data structures. Many
languages provide pointers not just to data but also functions or
procedures, i.e. to executable code. Thus, code pointers offer high
flexibility of code reconfiguration at runtime. Yet, their treatment
in specification and verification has been poor due to their
complexity. In order to write correct software in state-of-the-art
languages it is paramount to have logics that permit reasoning about
programs including function pointers.
Separation Logic has presented us with a handle to tackle the
complexity of pointers. It permits local reasoning on the heap,
liberating the verifier from specifying and proving that most of the
heap does not change when a procedure or command is executed.
The central objective of this project is to establish program (Hoare-)
logics for languages with explicit and implicit code pointers making
the benefits of Separation Logic amenable to them. The reasoning
principles developed are supposed to be implemented in a theorem prover.
For further information about the project see:
http://www.informatics.sussex.ac.uk/research/projects/PL4HOStore
The ideal candidate will have a relevant PhD, a strong grounding in
the field, and should have a background in one, or ideally several, of
the following areas: program logics, separation logic, denotational
semantics, (Hoare-) type theory, reflective programming (in the
context of object-oriented languages), mechanization of formal logics
in theorem provers.
Candidates must be eligible to work in the UK under EPSRC funding (the
project is funded by the EPSRC EP/G003173/1) and should expect to work
on-campus at the University of Sussex. The expected start date for the
project is, at earliest, 1 October 2008. All candidates must submit a
sample of their academic writing.
Enquiries should be addressed to Dr. Bernhard Reus ([EMAIL PROTECTED]
).
Closing date: 3 September 2008
Interviews will be held: 18/19 September 2008.
For full details and how to apply see www.sussex.ac.uk/jobs
