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

  • Welcome to Daniele Nantes, new researcher with the group

    Apr 26, 2022

    A very warm welcome to Daniele Nantes Sobrinho, who has joined the group as a research assistant. Daniele is a tenured assistant professor at the Department of Mathematics, University of Brasília, and is currently in a long sabbatical leave.

    more...

  • Talk at Rust Verification Workshop, ETAPS 2022

    Apr 4, 2022

    Sacha Ayoun and Petar Maksimovic gave a talk on Gillian-Rust: Unified Symbolic Analysis for Rust at the Second Rust Verification Workshop (RW2022), which was held in Munich, Germany, co-located with ETAPS 2022

    more...

  • Congratulations to Dr Sampaio

    Mar 29, 2022

    Many congratulations to Gabriela Sampaio, who defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS very succesfully today.

    more...

  • Philippa Gardner, talk at High Integrity Software (HIS) conference

    Nov 5, 2021

    Philippa gave a talk on Verified Trustworthy Software Specification at this year’s High Integrity Software (HIS) Conference.

    more...

  • Sacha Ayoun, internship with Amazon Web Services

    Nov 1, 2021

    Welcome back to Sacha who has returned from a three-months internship with the CodeGuru team at Amazon Web Services.

    more...

  • Recent Publications

    1. TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

      ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021., vol. 43(4)

    2. Gillian, Part II: Real-World Verification for JavaScript and C

      Proceedings of the 33rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II, pp. 827–850

    3. Two Mechanisations of WebAssembly 1.0

      Proceedings of the 24th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, pp. 61–79

    4. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

      Proceedings of the 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), pp. 31:1–31:23

    5. 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