[TYPES/announce] RA position in automated verification, logic and theorem proving at UCL

[James Brotherston]

*Research Associate positions in Automated Verification, Logic and 
Theorem Proving
*

*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".

Automatic verification tools based on separation logic have recently 
enabled the verification of code bases that scale into the millions of 
lines. Such analyses rely heavily on the use of inductive predicates to 
describe data structures held in memory.  However, these predicates must 
currently be hard-coded into the analysis, which means the analysis must 
fail when encountering a data structure not described by a hard-coded 
predicate. This project is about using *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 project will be run under the supervision of Dr. James Brotherston 
and Prof. Byron Cook, in the Programming Principles, Logic and 
Verification (PPLV) group at UCL. Other permanent PPLV members include 
Prof. David Pym, Dr. Jade Alglave and Dr. Juan Navarro Perez.  See 
pplv.cs.ucl.ac.uk for details.

The Research Associate post is funded full-time for 3 years, 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, or program logics, as evidenced by 
their work history and/or publication record. Expertise in inductive 
theorem proving, separation logic and/or program analysis techniques is 
particularly welcome, and prior experience in OcaML programming would 
also be beneficial.


The application closing date is *14 Feb 2014*, with interviews expected 
to be held in the period 25-28 February.


Further information on the position, including salary information and 
how to apply, may be found at: http://tinyurl.com/naqk5ze
*
*Informal enquiries may be made toJames Brotherston by email at 
**J.Brotherston at ucl.ac.uk .

<With apologies for any duplication of messages.  JB>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140114/c18152b5/attachment.html>