Formal verification
Overview
The formal verification theme covers foundational and applied research on mathematically rigorous proofs of the correctness and security of computing systems. This theme is crosscutting across computer science, as we build new theoretical foundations, verification frameworks, logics and tools such as model checkers. We apply these to formal verification of computer-science systems, algorithms, and artifacts: memory models, security protocols from foundational authenticated key-exchange to applicative ones such as e-voting to payments, distributed and concurrent algorithms, blockchain, safety-critical systems (e.g., railways).
We also provide national and international leadership on verification as a co-host of the NCSC Research Institute on Verified Trustworthy Software Systems (VeTSS), with Brijesh Dongol as co-Director jointly with Azalea Raad at Imperial College London.
Our members collaborate with a wide range of external stakeholders from academia, industry (Arm, Thales, Vodafone, Amazon, Nvidia, etc), and government (Dstl, NPL, NCSC, etc).
People
Theme lead
Professor Brijesh Dongol
Director of the UK Research Institute on Verified Trustworthy Software Systems (VeTSS)
Theme members
Professor Ioana Boureanu
Professor in Secure Systems & Head of Surrey Centre for Cyber Security (SCCS)
Professor Gregory Chockler
Professor in Computer Science
Dr Catalin Dragan
Lecturer in Secure Systems
Dr Sasa Radomirovic
Senior Lecturer in Secure Systems; Programme Lead of MSc Information Security
Professor Steve Schneider
Director of Computer Science Research Centre
Professor Helen Treharne
Head of School of Computer Science and Electronic Engineering; Professor in Computer Science SFHEA, FBCS
Ling Zhang
Technical Project Manager