[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Research
Associate positions in Verification, Logic and Theorem
Proving
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: 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 j.brothers...@ucl.ac.uk |