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

News

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. Fault-tolerant Resource Reasoning

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

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

  4. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

    Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS)

  5. A Trusted Mechanised Specification of JavaScript: One Year On

    Proceedings of the 27th International Conference on Computer Aided Verification (CAV)