This research group focuses on mechanised language specification and program verification. We are exploring what it means to build, evaluate, and trust a fully mechanised language specification, using JavaScript as the real-world example language. We are developing library specifications which must be robust with respect to the environment: implementations should not leak; and specifications should be useful to the client. We are developing compositional program reasoning techniques that scale, leading to automatic tools for verifying properties of programs. Our current focus is on modern concurrent separation logics, the development of tools for compositional symbolic analysis using the multi-language platform Gillian, and the specification and verification of Web programs. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course here.
Jun 16, 2020
There is an opening for at least one post-doctoral researcher in the Verified Software Group led by Professor Philippa Gardner. This position is initially for two years, with an option to extend in future. The funding from Philippa’s EPSRC Fellowship allows for a flexible start date in these uncertain times, in the academic year starting September 2020. Further funding is expected to be available over the next year. If interested, please contact Philippa directly as soon as possible.
May 19, 2020
This year’s PLDI has moved online and the organisers have just posted a song to remind attendees that virtually or not, this is still PLDI.
May 11, 2020
Congratulations to Jose Fragoso, Petar Maksimovic, Sacha Ayoun and Philippa Gardner, whose paper, Gillian, Part I: A Multi-language Platform for Symbolic Execution, has been accepted at this year’s PLDI.
Apr 27, 2020
Two papers by members of the group have been accepted at the 34th European Conference on Object-Oriented Programming, ECOOP 2020.
Feb 20, 2020
Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, Parametric Operational Semantics for Consistency Models today.
Gillian, Part I: A Multi-language Platform for Symbolic Execution
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15–20, 2020, London, UK
Parametric Operational Semantics for Consistency Models
Ph.D. Thesis, Imperial College London
Data Consistency in Transactional Storage Systems: a Centralised Approach
34th European Conference on Object-Oriented Programming (ECOOP 2020)
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications
34th European Conference on Object-Oriented Programming (ECOOP 2020)
(Submitted) TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs