[TYPES/announce] Research positions in Verification, Logic and Theorem Proving at University College London

[James Brotherston]

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Research Associate positions in Verification, Logic and Theorem Proving  The University College London (UCL) Dept. of Computer Science invites applications for two postdoctoral Research Associates (RAs) 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 James Brotherston and Byron Cook, in the Programming Principles, Logic and Verification (PPLV) group at UCL, which conducts world-leading research in the area of logic-based program verification.  Other researchers in this group include Peter O'Hearn, Thomas Dillig, Juan Navarro Perez and Jade Alglave.  For further details go to: http://pplv.cs.ucl.ac.uk The two RA posts are funded at full-time for 3 years, subject to satisfactory performance, and are available immediately.  We anticipate that one of the RAs will be more theoretically-focused, and the other more implementation-focused. 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. Information on the two postdoctoral RA positions, including how to apply (closing date: 22 August 2013), may be found at: http://tinyurl.com/k5c4x8v Informal enquiries may be made to James Brotherston by email at j.brothers...@ucl.ac.uk