Programming Principles, Logic, and Verification

Research in the PPLV group spans theory and practice, including logic, semantics, language design, program analysis, systems verification and systems modelling.

The goal of the group’s research is to produce mathematically rigorous concepts and techniques that aid in the construction and analysis of computer and information systems, and to make fundamental contributions to the underlying logic, mathematics, and computer science that supports our work.

We have outstanding connections with cutting-edge industry and excellent connections with other groups at UCL, including Systems and Networks, Information Security, and Software Systems Engineering.

Mechanized program verification, in particular, has seen a surge of interest in the research community in the past decade. This has been triggered by practical advances where in special domains – in avionics code, in device drivers, and other small systems programs – we have seen fully automated verification of selected properties such as memory safety and termination and API protocol conformance.

Our work on Separation Logic and the Space Invader tool, and on SLAM and Terminator, has played a part in this resurgence. We believe that these advances are suggestive of much more, of more general practical impact for verification and program analysis across the spectrum of computer systems.

Recent work on automatic verification can be seen as part of a larger trend in applied logic, where mathematical logic is moving from being a conceptual mathematical tool to a collection of techniques which can be used by practising engineers and scientists in solving the concrete problems that they face.

Another example of this trend is provided by our work in systems and security modelling, including work on access control policies and models.

Techniques from semantics (e.g., process algebra) and logic (e.g., modal and substructural) have been developed to provide a basis for systems modelling tools, such as Gnosis, that deploy these ideas in the style of classical mathematical modelling – as practised in engineering, economics, and so on – to understand the interaction between system architecture and security policy.

Building on our core research, part of the aim of the PPLV group is applied logic outreach, in areas such as program verification, artificial intelligence, security, biology, and economics.

Projects

PPLV staff members and students are currently involved in the following projects:

Algebra and Logic for Policy and Utility in Information Security
David Pym (PI), J. Swierzbinski, M.J. Collinson, G. McCusker, C. Ioannidis and P. Cornish.
Dec 2013 — Nov 2017.

Productive Security - Improving security compliance and productivity through measurement
A Sasse (PI) and David Pym.
Oct 2012 — Mar 2016.

Resource Reasoning
David Pym (PI) and Byron Cook.
Mar 2012 — Jun 2016.

Boosting Automated Verification using Cyclic Proof
James Brotherston (PI), Byron Cook and N Gorogiannis.
Nov 2013 — May 2017.

Logical Foundations of Resource
James Brotherston (PI).
Jun 2012 — Nov 2016.

Compositional Security Analysis for Binaries
Byron Cook (PI).
Nov 2013 — Nov 2016.

Program Verification Techniques for Understanding Security Properties of Software
B. Karp (PI), Juan Navarro Perez, M.J. Handley, and Byron Cook.
Oct 2013 — Oct 2016.

Partial order semantics for concurrent program verification
Jade Alglave (PI).
Feb 2014 — Feb 2016

Automating Separation Logic Reasoning
Juan Navarro Perez (PI).
Jan 2014 — Jun 2015

People

Academic Staff

Richard Bornat (Visiting Professor)
James Brotherston (Senior Lecturer / EPSRC Research Fellow)
Byron Cook (Joint appointment with Amazon)
Robin Hirsch (Professor of Mathematical Foundations of Computing)
Peter O’Hearn (Professor of Computer Science, on leave at Facebook, part-time at UCL)
David Pym (Professor of Information, Logic, and Security, Head of Group)
Alexandra Silva (Senior Lecturer/ERC grant holder)
Ilya Sergey (Lecturer)
Fabio Zanasi (Lecturer)