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

  • Welcome to Martin Bodin, new member of the group

    Jun 13, 2018

    We are very happy to welcome Martin Bodin, who joins the group as a Research Associate. Martin did his PhD on Certified Semantics and Analysis of JavaScript at the University of Rennes 1 under the supervision of Alan Schmitt and Thomas Jensen. He then participated on the JSCert project to build a Coq specification for JavaScript.

    more...

  • Welcome to Felix Stutz

    Apr 23, 2018

    We are very pleased to welcome Felix Stutz, an MSc student at the International Max Planck Research School for Computer Science, who is due to spend five months with the group, working with Emanuele D’Osualdo on Ideal completions for Verification of Cryptographic Protocols.

    more...

  • Paper accepted and paper published

    Apr 18, 2018

    A paper co-authored by current and former researchers of the group has just been publised. A second paper, also collaborative work with current and former researchers has also just been accepted to ECOOP 18.

    more...

  • Formal Methods Meets JavaScript Workshop

    Mar 19, 2018

    On Monday 19th March, we hosted 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.

    more...

  • Congratulations to Dr Daiva Naudžiūnienė

    Mar 1, 2018

    Many congratulations to Daiva Naudžiūnienė, who very successfully defended her PhD thesis, An Infrastructure for Tractable Verification of JavaScript Programs on Monday 1st March.

    more...

  • Recent Publications

    1. A Perspective on Specifying and Verifying Concurrent Modules

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

    2. A Concurrent Specification of POSIX File Systems

      32nd European Conference on Object-Oriented Programming (ECOOP 2018).

    3. JSExplain: a Double Debugger for JavaScript

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

    4. JaVerT: JavaScript Verification Toolchain

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

    5. An Infrastructure for Tractable Verification of JavaScript Programs

      Ph.D. Thesis, Imperial College London