[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
[Please share with possible candidates, especially graduating Master’s students
in relevant areas. Thank you, and apologies for cross-postings.]
PhD studentship in logic and systems verification at UCL [Apologies, corrected
start-date: October 2019]
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:
- Logic
- Verification
- Systems modelling.
The studentship is aligned with the IRIS project
(https://uclirisproject.wordpress.com<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>),
--- 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 2019.
Candidates should be UK or EU nationals.
Interested candidates may contact David Pym
([email protected]<mailto:[email protected]>) or James Brotherston
([email protected]<mailto:[email protected]>) 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
[email protected]<mailto:[email protected]>
www.cs.ucl.ac.uk/people/D.Pym.html<http://www.cs.ucl.ac.uk/people/D.Pym.html>
www.cs.ucl.ac.uk/staff/D.Pym/<http://www.cs.ucl.ac.uk/staff/D.Pym/>
Assistant: Julia Savage, [email protected]<mailto:[email protected]>, +44
(0)20 7679 0327
