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 reasoning about JavaScript and Concurrency. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course here.

JavaScript Concurrency

Recent News

  • 8th Conference on Algebra and Coalgebra in Computer Science

    Jun 3, 2019

    Philippa Gardner and Emanuele D’Osualdo are part of the local organising team for the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) which is taking place in London this week.

    more...

  • Goodbye to Dr Andrea Cerone.

    May 31, 2019

    Our very best wishes to Andrea Cerone, who after three years with the group is leaving to take up a position as a software engineer for Footballradar.

    more...

  • Effective Verification Workshop at the Lorentz centre, talks by Philippa Gardner and Emanuele D’Osualdo

    May 13, 2019

    Philippa Gardner and Emanuele D’Osualdo gave invited talks as this May’s Lorentz centre workshop: Effective Verification: Static Analysis Meets Program Logics in Leiden, The Netherlands.

    more...

  • Talk at Formal Methods for Statistical Software workshop, Martin Bodin

    May 1, 2019

    Martin Bodin gave a talk “A Trustworthy Mechanized Formalization of R“ at the Formal Methods for Statistical Software (FMfSS 2019) workshop, to present his work on big-step operational semantics for R. The abstract for the talk is below.

    more...

  • Paper accepted at ECOOP 2019

    Apr 1, 2019

    Congratulations to Petar Maksimović and Philippa Gardner, whose paper with Conrad Watt and Neel Krishnaswami (University of Cambridge) has been accepted at this year’s European Conference on Object-Oriented Programming (ECOOP ‘19)

    more...

  • Recent Publications

    1. A Program Logic for First-Order Encapsulated WebAssembly

      Proceedings of the 33 rd European Conference on Object-Oriented Programming (ECOOP’19). , pp. 10:1–10:30

    2. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

      PACMPL, vol. 3( POPL)

    3. Skeletal Semantics and their Interpretations

      PACMPL, vol. 3( POPL)

    4. Symbolic Execution for JavaScript

      Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 11:1–11:14

    5. JaVerT: JavaScript Verification and Testing Framework: Invited Talk

      Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 1:1–1:4