coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] RA position in automated verification, logic and theorem proving at UCL

From: James Brotherston <J.Brotherston AT cs.ucl.ac.uk>
To: types-announce AT lists.seas.upenn.edu, ProofTheory.List AT gmail.com, theorem-provers AT ai.mit.edu, theory-logic AT cs.cmu.edu, cl-isabelle-users AT lists.cam.ac.uk, coq-club AT inria.fr, lfcs-interest AT inf.ed.ac.uk, prog-lang AT diku.dk, research AT cs.ucl.ac.uk, cade AT itu.dk, logic-list AT helsinki.fi, theory-a AT listserv.nodak.edu
Subject: [Coq-Club] RA position in automated verification, logic and theorem proving at UCL
Date: Tue, 14 Jan 2014 16:14:44 +0000

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 to James Brotherston by email at J.Brotherston AT ucl.ac.uk .

<With apologies for any duplication of messages. JB>

[Coq-Club] RA position in automated verification, logic and theorem proving at UCL, James Brotherston, 01/14/2014