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

  • Papers accepted at POPL 2019

    Nov 10, 2018

    Congratulations to José Fragoso Santos, Philippa Gardner, Petar Maksimović, Martin Bodin and Gaby Sampaio, whose papers were accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).


  • Welcome to Sacha Ayoun, new PhD student with the group

    Oct 15, 2018

    We are very happy to welcome Sacha Ayoun, who has joined the group as a PhD student.


  • Talk by Emma Tye, UROP student with the group, AVL tree algorithms

    Oct 10, 2018

    Emma Tye, a 2nd year UROP student working with Philippa Garner and Jose Fragoso on JaVerT, presented her work at this year’s first group’s Wednesday meeting.


  • IBM Project Prize to Radu Szasz, Msc project supervised by Philippa Gardner and Jose Fragoso

    Sep 3, 2018

    Congratulations to Radu Szasz (MEng Computing Year 4), who was awarded the IBM Project Prize for his MsC project, Typing JavaScript via Symbolic Execution, supervised by Philippa Gardner and Jose Fragoso.


  • Seminar by Felix Stutz on Automated Verification of Security Protocols

    Jul 16, 2018

    Felix Stutz gave a talk on Monday on Automated Verification of Security Protocols. He presented the latest work on the project he is doing with Emanuele D’Osualdo and which will inform his Master Thesis.


  • Recent Publications

    1. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

      PACMPL, vol. 3( POPL)

    2. Skeletal Semantics and their Interpretations

      PACMPL, vol. 3( POPL)

    3. Symbolic Execution for JavaScript

      Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 11:1–11:14

    4. A Perspective on Specifying and Verifying Concurrent Modules

      Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25

    5. A Concurrent Specification of POSIX File Systems

      32nd European Conference on Object-Oriented Programming (ECOOP 2018).