[TYPES/announce] PostDoc Position in Program Verification

[Bernhard Reus]

[ 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 (bernhard at sussex.ac.uk 
).

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

  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20080729/f2b423be/attachment-0001.htm