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

  • Formal Methods Meets JavaScript Workshop

    Mar 14, 2018

    On Monday 19th March, we’re hosting a day of research talks on Programming Languages Formal Methods researchers on topics including language specification, program verification, etc. with a focus on research relating to the JavaScript language and ecosystem.


  • Paper presented at POPL18

    Jan 12, 2018

    José Fragoso Santos prsented his paper JaVerT: JavaScript Verification using Separation Logic, jointly authored with Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood and Philippa Gardner, at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).


  • PhD position, start date in October 2018

    Jan 6, 2018

    Philippa Gardner is currently looking for a PhD student, start date in October 2018, to join the Verified Trustworthy Software Specification Group,


  • Visitor to the group, Siddharth Krishna, New York University, USA

    Nov 24, 2017

    We are very pleased to have welcomed Siddharth Krishna, from the Courant Institute of Mathematical Sciences, NYU, who visited the group this week to talk about his work on the verification of concurrent data structures.


  • Visitor to the group, Giovanni Bernardi, IRIF, Paris

    Nov 15, 2017

    Dr Giovanni Bernardi of Paris Diderot University / IRIF visited the group in November to give a talk on his current work on must- testing for message passing concurrency.


  • Recent Publications

    1. JSExplain: a Double Debugger for JavaScript

      WWW ’18 Companion: The 2018 Web Conference Companion, April 23–27, 2018, Lyon, France

    2. JaVerT: JavaScript verification toolchain

      PACMPL, vol. 2(POPL), pp. 50:1–50:33

    3. Algebraic Laws for Weak Consistency

      Proceedings of 28th International Conference on Concurrency Theory, (Concur 2017)

    4. Verified trustworthy software systems

      Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, vol. 375(2104)

    5. Towards Logic-based Verification of JavaScript Programs

      Proceedings of 26th Conference on Automated Deduction (CADE 26)