<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class=""><br class="">
</div>
<div class="">
<div class="">[Please share with possible candidates, especially graduating Master’s students </div>
<div class="">in relevant areas. Thank you, and apologies for cross-postings.] </div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class="">PhD studentship in logic and systems verification at UCL [Apologies, corrected </div>
<div class="">start-date: October 2019]</div>
<div class=""><br class="">
</div>
<div class="">We are looking to hire an exceptionally able and highly-motivated PhD student in the <br class="">
area of logic and verification to work in UCL's PPLV group. We are particularly keen <br class="">
to find someone who is interested in systems modelling and verification and their <br class="">
underlying logical theory: </div>
<div class=""><br class="">
</div>
<div class="">- Logic</div>
<div class="">- Verification</div>
<div class="">- Systems modelling. <br class="">
<br class="">
The studentship is aligned with the IRIS project (<a href="https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fuclirisproject.wordpress.com&data=02%7C01%7Cd.pym%40ucl.ac.uk%7Cee5c90844fed4a04ee9e08d6cfe1ef83%7C1faf88fea9984c5b93c9210a11d9a5c2%7C0%7C0%7C636924966622963549&sdata=7n9sIoV7rmG27Syu00JCpMNLW4EYX7zWXrfSmQM4U3A%3D&reserved=0" originalsrc="https://uclirisproject.wordpress.com" shash="iat8WnlQ5ZUGCZ0tHRSADDwz2xdwDG7xZDWEyIbLaB1COO+IPD4IM6+sE9Hx7fiBjnR0WDXhkNnGJ4UYFtXZWSW3QcDug/77FF/c9Uq2N94nhDVIU9bC37tXVtOFhtfmSQgPxfVl9fX82EJgLKElSq3kcm2KCfpLcZPOXP0P4zY=" class="">https://uclirisproject.wordpress.com</a>), <br class="">
--- which is focussed on understanding and reasoning about the compositional structure <br class="">
of systems models and the supporting idea of an interface --- and will be supervised by </div>
<div class="">Professor David Pym (<a href="http://www.cs.ucl.ac.uk/staff/D.Pym/" class="">http://www.cs.ucl.ac.uk/staff/D.Pym/</a>) and Dr. James Brotherston </div>
<div class="">(<a href="http://www0.cs.ucl.ac.uk/staff/J.Brotherston/" class="">http://www0.cs.ucl.ac.uk/staff/J.Brotherston/</a>). <br class="">
<br class="">
In more detail, area of the studentship is in logic and its application to program and <br class="">
systems verification, with a particular interest in the development and application of <br class="">
logical tools based on bunched logic, separation logic, and concurrent separation logic <br class="">
(and related ideas) and their use to reason about the correctness of interfaces between <br class="">
programs, systems, and organizations. The project may range from theoretical work <br class="">
in logic (semantics and proof theory) through the theory of system modelling tools to the <br class="">
design and implementation of modelling and verification tools. <br class="">
<br class="">
The PPLV group conducts world-leading research in logical and algebraic methods and <br class="">
their applications to program and systems modelling and verification. The Interface <br class="">
Reasoning for Interacting Systems (IRIS) project, led by Prof. David Pym, uses logical <br class="">
and algebraic methods to understand the compositional structure of systems and their <br class="">
communications, seeking to develop analyses at all scales, from code through distributed <br class="">
systems to organizational structure, generically and uniformly. <br class="">
<br class="">
The IRIS project, funded as a UK EPSRC Programme Grant, is a collaboration involving <br class="">
James Brotherston, Byron Cook, George Danezis, Peter O’Hearn, and David Pym at UCL, <br class="">
Alastair Donaldson at Imperial College, Will Venters at LSE, and Edmund Robinson at <br class="">
QMUL. Industry partners include Amazon AWS, BT, Facebook, HP Labs, GridPP, and Methods <br class="">
Group. <br class="">
<br class="">
Candidates should normally have or be about to complete a Master's level qualification in <br class="">
mathematics or computer science, with a strong component in logic or theoretical computer <br class="">
science. <br class="">
<br class="">
The student is available with an earliest start-date of October 2019. <br class="">
Candidates should be UK or EU nationals. <br class="">
<br class="">
Interested candidates may contact David Pym (<a href="mailto:d.pym@ucl.ac.uk" class="">d.pym@ucl.ac.uk</a>) or James Brotherston <br class="">
(<a href="mailto:j.brotherston@ucl.ac.uk" class="">j.brotherston@ucl.ac.uk</a>) for more information. <br class="">
<br class="">
To apply, please follow the instructions at <br class="">
<a href="http://www.cs.ucl.ac.uk/prospective_students/phd_programme/applying/" class="">http://www.cs.ucl.ac.uk/prospective_students/phd_programme/applying/</a><br class="">
<br class="">
<br class="">
--<br class="">
Professor of Information, Logic, and Security <br class="">
Head of Programming Principles, Logic, and Verification<br class="">
University College London<br class="">
<br class="">
<a href="mailto:d.pym@ucl.ac.uk" class="">d.pym@ucl.ac.uk</a><br class="">
<a href="http://www.cs.ucl.ac.uk/people/D.Pym.html" class="">www.cs.ucl.ac.uk/people/D.Pym.html</a><br class="">
<a href="http://www.cs.ucl.ac.uk/staff/D.Pym/" class="">www.cs.ucl.ac.uk/staff/D.Pym/</a><br class="">
<br class="">
Assistant: Julia Savage, <a href="mailto:j.savage@ucl.ac.uk" class="">j.savage@ucl.ac.uk</a>, +44 (0)20 7679 0327</div>
</div>
</body>
</html>