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. Much of our work is based on Separation Logic. See details of our fourth-year/MSc course here.

JavaScript Concurrency

Recent News

  • Welcome to Gabriela Sampaio, new PhD student with the group

    Oct 2, 2017

    We are really happy to welcome Gabriela Sampaio, who has joined the group as a PhD student.


  • Paper accepted at POPL 2018

    Sep 26, 2017

    José Fragoso Santos, Philippa Gardner, Petar Maksimović, Daiva Naudžiūnienė and Thomas Wood, have had a paper accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).


  • Fifth Workshop on Formal Methods and Tools for Security (FMATS5)

    Sep 22, 2017

    Almost a hundred participants attended this year’s FMATS, held on 21-22 September 2017 at Microsoft Research Cambridge.


  • Philippa Gardner, Keynote talk at Reliably Secure Software Systems (RS3) meeting, Darmstadt, Germany.

    Sep 6, 2017

    Philippa Gardner gave a keynote talk entitled ‘Trustworthy Software Specification’ at the final event of the DFG-funded national research initiative “Reliably Secure Software Systems (RS3)”.


  • Invited paper at the 26th International Conference on Automated Reasoning, (CADE), Gothenburg, Sweden.

    Aug 12, 2017

    Philippa Gardner was one of the invited speakers at the this year’s CADE conference, held in Gothenburg, Sweden, on 6-11 August 2017.


  • Recent Publications

    1. Algebraic Laws for Weak Consistency

      Proceedings of 28th International Conference on Concurrency Theory, (Concur 2017)

    2. Towards Logic-based Verification of JavaScript Programs

      Proceedings of 26th Conference on Automated Deduction (CADE 26)

    3. Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

      Proceedings of 30th IEEE Computer Security Foundations Symposium, (CSF 2017)

    4. Abstraction, Refinement and Concurrent Reasoning

      Ph.D. Thesis, Imperial College London

    5. Reasoning with Time and Data Abstractions

      Ph.D. Thesis, Imperial College London