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

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

  • Papers accepted at POPL 2019

    Nov 10, 2018

    Congratulations to José Fragoso Santos, Philippa Gardner, Petar Maksimović, Martin Bodin and Gaby Sampaio, whose papers were accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).

    more...

  • Welcome to Sacha Ayoun, new PhD student with the group

    Oct 15, 2018

    We are very happy to welcome Sacha Ayoun, who has joined the group as a PhD student.

    more...

  • Recent Publications

    1. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

      PACMPL, vol. 3( POPL)

    2. Skeletal Semantics and their Interpretations

      PACMPL, vol. 3( POPL)

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

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

    5. A Perspective on Specifying and Verifying Concurrent Modules

      Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25