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


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


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


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


  • Talk by Dr Justin Hsu, From Couplings to Probabilistic Relational Program Logics

    Feb 14, 2018

    Dr Justin Hsu of University College of London visited the group this week to give a talk about probabilistic coupling: “From Couplings to Probabilistic Relational Program Logics”.


  • 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. JSExplain: a Double Debugger for JavaScript

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

    3. JaVerT: JavaScript verification toolchain

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

    4. An Infrastructure for Tractable Verification of JavaScript Programs

      Ph.D. Thesis, Imperial College London

    5. Algebraic Laws for Weak Consistency

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