[TYPES/announce] PhD studentship in logic and verification at UCL

[Pym, David]

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 (https://uclirisproject.wordpress.com), 
--- 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 (http://www.cs.ucl.ac.uk/staff/D.Pym/)and 
Dr. James Brotherston (http://www0.cs.ucl.ac.uk/staff/J.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. 

The PPLV group conducts world-leading research in logical and algebraic methods and 
their applications to program and systems modelling and verification. The Interface 
Reasoning for Interacting Systems (IRIS) project, led by Prof. David Pym, uses logical 
and algebraic methods to understand the compositional structure of systems and their 
communications, seeking to develop analyses at all scales, from code through distributed 
systems to organizational structure, generically and uniformly. 

The IRIS project, funded as a UK EPSRC Programme Grant, is a collaboration involving 
James Brotherston, Byron Cook, George Danezis, Peter O’Hearn, and David Pym at UCL, 
Alastair Donaldson at Imperial College, Will Venters at LSE, and Edmund Robinson at 
QMUL. Industry partners include Amazon AWS, BT, Facebook, HP Labs, GridPP, and Methods 
Group. 

Candidates should normally have or be about to complete a Master's level qualification in 
mathematics or computer science, with a strong component in logic or theoretical computer 
science. 

The student is available with an earliest start-date of October 2018. 
Candidates should be UK or EU nationals. 

Interested candidates may contact David Pym (d.pym at ucl.ac.uk) or James Brotherston 
(j.brotherston at ucl.ac.uk) for more information. 

To apply, please follow the instructions at 
http://www.cs.ucl.ac.uk/prospective_students/phd_programme/applying/


--
Professor of Information, Logic, and Security 
Head of Programming Principles, Logic, and Verification
University College London

d.pym at ucl.ac.uk
www.cs.ucl.ac.uk/people/D.Pym.html
www.cs.ucl.ac.uk/staff/D.Pym/

Assistant: Julia Savage, j.savage at ucl.ac.uk, +44 (0)20 7679 0327