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

  • Visit from Alan Schmitt, Inria, France

    Feb 20, 2017

    Alan Schmitt, a researcher in the Celtique team at Inria in Rennes visited the group this week. Alan’s research focuses on the certification of semantics and static analyses, in particular the semantics of JavaScript and analyses based on abstract interpretation.

    more...

  • 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...

  • Congratulations to Azalea Raad on her viva

    Feb 10, 2017

    Congratulations to Azalea Raad who very successfully defended her PhD thesis, Abstraction, Refinement and Concurrent Reasoning on Friday 10 February.

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

  • 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