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

  • JSExplain discussed at ECMAScript standards committee meeting

    Dec 5, 2016

    Thomas Wood attended the latest ECMAScript standards committee TC39 meeting this November in San Francisco.


  • Talk at Dagstuhl Seminar

    Nov 23, 2016

    Andrea Cerone was invited to attend the seminar on Concurrency with Weak Memory Models at Schloss Dagstuhl last week.


  • Infer Lab at Imperial

    Nov 14, 2016

    The Separation Logic course team ran a lab on Infer, an automatic verification tool based on separation logic, developed at Facebook where it is used every day to verify millions of lines of code.


  • Keynote talk at the IET SSCS Conference

    Oct 12, 2016

    Philippa Gardner was one of the keynote speakers at the 11th System Safety and Cyber Security Conference, (SSCS 2016) organised by the IET.


  • Papers published by Azalea Raad

    Oct 3, 2016

    Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, APLAS 2016.


  • Recent Publications

    1. Modular Termination Verification for Non-blocking Concurrency

      Proceedings of the 25th European Symposium on Programming (ESOP)

    2. Verifying Concurrent Graph Algorithms

      Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings

    3. DOM: Specification and Client Reasoning

      Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings

    4. Fault-tolerant Resource Reasoning

      Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS)

    5. Reasoning about the POSIX File System: Local Update and Global Pathnames

      Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)