[TYPES/announce] Postdoc position at UCL in verification / logic / automated reasoning

[James Brotherston]

Research Associate position in Automated Verification, Logic and Theorem 
Proving (ref:1439542)
Dept. of Computer Science, University College London, UK


The UCL Dept. of Computer Science invites applications for a 
postdoctoral Research Associate to work on the EPSRC-funded project 
"Boosting Automated Verification using Cyclic Proof".

The core of the project is the use of *cyclic proof*, a relatively new 
technique in inductive theorem proving, to add general inductive 
reasoning capability to the various components of interprocedural 
program analysis and thereby, hopefully, to extend the reach of current 
verification methods.  The main experimental tool is the cyclic theorem 
prover Cyclist (see https://github.com/ngorogiannis/cyclist ).

The project is under the supervision of Dr. James Brotherston in the 
Programming Principles, Logic and Verification (PPLV) group at UCL; 
others involved in the project include Prof. Byron Cook and Dr. Reuben 
Rowe at UCL, and Dr. Nikos Gorogiannis at Middlesex University. For 
further information about the PPLV group, see http://pplv.cs.ucl.ac.uk .

The Research Associate post is funded full-time until *10 May 2017*, and 
is available immediately.

Applicants must hold, or be about to hold, a PhD in computer science or 
a closely related field, and should have a strong background in 
verification, automated reasoning, and/or program logics, as evidenced 
by their work history and/or publication record. Expertise in inductive 
theorem proving, separation logic and program analysis techniques is 
particularly welcome, and prior experience in OcaML programming would 
also be beneficial.

The application closing date is *Fri 14 Nov, 2014*, with interviews 
expected to be held in the week beginning *Mon 1 Dec*.

Further information on the position, including salary information and 
how to apply, may be found at:

http://tinyurl.com/mgvvdbu

Informal enquiries may also be made toJames by email at 
J.Brotherston at ucl.ac.uk .