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


Talk at Dagstuhl Seminar

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

Infer Lab at Imperial

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

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

Papers publised by Azalea Raad

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

Daiva Naudžiūnienė moving to Facebook

Congratulations to Daiva Naudžiūnienė, who is off to work for Facebook in the new year.

Welcome to Andrea Cerone, new member of the group

We are very happy to welcome Andrea Cerone to the group. Andrea has joined us from the IMDEA Software Institute, Madrid, Spain, where he worked with Dr. Alexey Gotsman on Verification of Higher Order Concurrent Libraries and Foundations of Consistency Models for Distributed Databases.

One new postdoc position at Imperial College

We are looking to recruit one postdoctoral researcher in the Program Specification and Verification Group at Imperial College London, to work on reasoning about concurrent programs. The position is suitable for either a theoretician, who would work on the foundations of concurrent reasoning, or a theoretician/practitioner, who would work on the verification and testing of file systems.

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)