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.

Concurrency Gillian Web Programs

Recent News

  • Post-doc Position(s) Available

    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.


  • PLDI 2020 song and REMS and DeepSpec workshop

    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.


  • Paper accepted at PLDI 2020

    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.


  • Papers accepted at ECOOP 2020

    Apr 27, 2020

    Two papers by members of the group have been accepted at the 34th European Conference on Object-Oriented Programming, ECOOP 2020.


  • Congratulations to Dr Shale Xiong

    Feb 20, 2020

    Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, Parametric Operational Semantics for Consistency Models today.