PPLV Group April 2019

Research in the PPLV group spans theory and practice, including logic, semantics, category theory, (co)algebra, automata theory, language design, program analysis, program verification, systems verification, concurrency, systems modelling, compilation, and theorem proving.

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. 



This page was last modified on 30 May 2019.