PhD Studentship in Logic and Systems Verification at UCL, Londen (UK)

We are looking to hire an exceptionally able and highly-motivated PhD student in the area of logic and verification to work in UCL's PPLV group. We are particularly keen to find someone who is interested in systems modelling and verification and their underlying logical theory. The studentship is aligned with the IRIS project which is focussed on understanding and reasoning about the compositional structure of systems models and the supporting idea of an interface --- and will be supervised by Professor David Pym and Dr. James Brotherston.

In more detail, area of the studentship is in logic and its application to program and systems verification, with a particular interest in the development and application of logical tools based on bunched logic, separation logic, and concurrent separation logic (and related ideas) and their use to reason about the correctness of interfaces between programs, systems, and organizations. The project may range from theoretical work in logic (semantics and proof theory) through the theory of system modelling tools to the design and implementation of modelling and verification tools.