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 Publications

  1. Symbolic Debugging with Gillian

    Proceedings of the 1st ACM International Workshop on Future Debugging Techniques, pp. 1–2

  2. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding

    37th European Conference on Object-Oriented Programming (ECOOP 2023), pp. 19:1–19:27

  3. Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

    44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023), pp. 151:1–151:25

  4. A Trusted Infrastructure for Symbolic Analysis of Event-based Web APIs

    Ph.D. Thesis, Imperial College London

  5. A Certified Algorithm for AC-Unification

    • Mauricio Ayala-Rincón
    • Maribel Fernández
    • Gabriel Ferreira Silva
    • Daniele Nantes

    7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 8:1–8:21