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.

JavaScript Concurrency

Recent News

  • Philippa Gardner, invited to give a talk at the Ecma TC39 meeting, Google, NY

    May 25, 2017

    Philippa Gardner was invited to talk about JavaScript Verification at the [TC39 – ECMAScript Task group standards committee meeting] (http://www.ecma-international.org/memento/TC39-RF-TG.htm) this May, held at Google, New York.

    more...

  • Farewell to Azalea Raad, joining the Max Planck Institute for Software Systems, Germany

    May 25, 2017

    Our best wishes to Dr Azalea Raad, who has accepted a position as a Postdoctoral Fellow at the Max Planck Institute for Software Systems in Kaiserslautern, Germany, starting in July.

    more...

  • Goodbye to Dr Gian Ntzik, moving to Amadeus

    May 17, 2017

    Best wishes to Dr Gian Ntzik, who will move to Amadeus at the end of May to work in systems development and research.

    more...

  • 6th South of England Regional Programming Language Seminar, UCL

    May 15, 2017

    The 6th edition of S-REPLS, organised by our colleague Ilya Sergey will take place on May 25, 2017, at University College London.

    more...

  • Johannes Kloss, visitor from MPI

    May 9, 2017

    Johannes Kloss, a fourth-year PhD student at the Max Planck Institute for Software Systems visited the group this week.

    more...

  • Recent Publications

    1. Caper: Automatic Verification for Fine-grained Concurrency

      Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 420–447

    2. Abstract Specifications for Concurrent Maps

      Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 964–990

    3. Modular Termination Verification for Non-blocking Concurrency

      Proceedings of the 25th European Symposium on Programming (ESOP’16), pp. 176–201

    4. Verifying Concurrent Graph Algorithms

      Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 314–334

    5. DOM: Specification and Client Reasoning

      Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422