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

  • Demo on the use of JaVerT at the JSTools'17 workshop

    Jul 7, 2017

    José Fragoso Santos gave a talk and demo on the use of JaVerT at the JSTools’17 workshop, part of this year’s European Conference on Object-Oriented Programming (ECOOP 2017).

    more...

  • Paper accepted at Concur 2017

    Jun 16, 2017

    Andrea Cerone has had a paper accepted at this year’s International Conference on Concurrency Theory, (Concur 2017) which will be held in Berlin, Germany in September.

    more...

  • Paper accepted at CSF'17

    Jun 13, 2017

    Emanuele D’Osualdo has had a paper accepted at this year’s Computer Security Foundations Symposium (CSF).

    more...

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

    May 25, 2017

    Philippa Gardner was invited to give a talk about JavaScript Verification at the TC39 – ECMAScript Task group standards committee meeting held at Google, New York, this May.

    more...

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

    May 25, 2017

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

  • Recent Publications

    1. Algebraic Laws for Weak Consistency

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

    2. Towards Logic-based Verification of JavaScript Programs

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

    3. Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

      Proceedings of 30th IEEE Computer Security Foundations Symposium, (CSF 2017)

    4. Caper: Automatic Verification for Fine-grained Concurrency

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

    5. Abstract Specifications for Concurrent Maps

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