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

  • National Cyber Security Centre (NCSC) official opening

    Feb 14, 2017

    Philippa Gardner attended the official opening by the Queen of the National Cyber Security Centre new headquarters in London. The NCSC, part of GCHQ, aims to make their work on cyber security more open; it will publish research, organise events and will provide advice on cyber security to businesses and members of the public.

    more...

  • Third edition of the Introduction to Verification and Testing (INVEST) workshop

    Feb 11, 2017

    Over sixty people attended the Introduction to Verification and Testing workshop, held this week at Imperial College London. The INVEST workshop, organised by Alastair Donaldson, Christian Cadar and Philippa Gardner gives young researchers and final year students with an interest in research the chance to take a closer look at the fields of software verification and testing.

    more...

  • Papers accepted at ESOP 2017

    Feb 6, 2017

    Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming (ESOP 2017), which will take place this April in Uppsala, Sweden. The first paper, Abstract Specifications for Concurrent Maps, present the importance of abstract atomicity for reasoning fine-grained concurrent modules. The second paper, Caper: Automatic Verification for Fine-grained Concurrency, presents a prototype tool for automated reasoning about concurrent modules.

    more...

  • Congratulations to Gian Ntzik on his viva

    Feb 1, 2017

    Congratulations to Gian Ntzik on successfully defending his PhD thesis, Reasoning about POSIX File Systems and many thanks to Ally Donaldson and Hongseok Yang who acted as examiners.

    more...

  • Talk at Principles in Practice (PiP), POPL 2017

    Jan 20, 2017

    Philippa gave a talk entitled An Infrastructure for Tractable Verification of JavaScript Programs at this year’s Principles in Practice workshop (PiP).

    more...

  • Recent Publications

    1. Caper: Automatic Verification for Fine-grained Concurrency

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

    2. Abstract Specifications for Concurrent Maps

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

    3. Modular Termination Verification for Non-blocking Concurrency

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

    4. Verifying Concurrent Graph Algorithms

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

    5. DOM: Specification and Client Reasoning

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