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

  • Daniele Nantes, co-chair of this year’s Women in Logic (WiL) workshop

    Aug 4, 2022

    Daniele is one of the co-chairs of this year’s Women in Logic 2022 (WiL), a co located event part of the 8th Federated Logic Conference (FLoC 2022) to be held in Haifa, Israel, this summer 2022.


  • Philippa Gardner, Keynote at Advances in Separation Logics (ASL 2022)

    Aug 1, 2022

    Philippa was one of the two keynote speakers at this year’s Advances in Separation Logics (ASL 2022) workshop, which was held online.


  • Concurrency meeting at the Isaac Newton Institute in Cambridge, August 2022

    Jul 26, 2022

    John Wickerson, Azalea Raad, Philippa Gardner and Andreas Lööw are the organisers of this year’s UK Concurrency Workshop. which will be held on 11-12 August 2022 at the Isaac Newton Institute (INI) in Cambridge.


  • Vistas in Verified Software, workshop at the Isaac Newton Institute, talks live-streamed

    Jun 30, 2022

    Philippa Gardner is one of the organisers, together with Azadeh Farzan, Natarajan Shankar and Moshe Vardi, of the Vistas in Verified Software workshop which will take place at the Isaac Newton Institute (INI) on 4-8 July 2022.


  • Daniele Nantes, paper published, TYPES

    Jun 14, 2022

    Daniele’s paper Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes has been published as part of the proceedings of the 27th International Conference on Types for Proofs and Programs,(TYPES), organised by the Leiden Institute of Advanced Computer Science, in the Netherlands.


  • Recent Publications

    1. Exact Separation Logic (submitted)

    2. 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)

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

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

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