[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
*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.brothers...@ucl.ac.uk .
<With apologies for any duplication of messages. JB>
