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.
Jun 3, 2019
Philippa Gardner and Emanuele D’Osualdo are part of the local organising team for the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) which is taking place in London this week.
May 31, 2019
Our very best wishes to Andrea Cerone, who after three years with the group is leaving to take up a position as a software engineer for Footballradar.
May 13, 2019
Philippa Gardner and Emanuele D’Osualdo gave invited talks as this May’s Lorentz centre workshop: Effective Verification: Static Analysis Meets Program Logics in Leiden, The Netherlands.
May 1, 2019
Martin Bodin gave a talk “A Trustworthy Mechanized Formalization of R“ at the Formal Methods for Statistical Software (FMfSS 2019) workshop, to present his work on big-step operational semantics for R. The abstract for the talk is below.
Apr 1, 2019
Congratulations to Petar Maksimović and Philippa Gardner, whose paper with Conrad Watt and Neel Krishnaswami (University of Cambridge) has been accepted at this year’s European Conference on Object-Oriented Programming (ECOOP ‘19)
A Program Logic for First-Order Encapsulated WebAssembly
Proceedings of the 33 rd European Conference on Object-Oriented Programming (ECOOP’19). , pp. 10:1–10:30
JaVerT 2.0: Compositional Symbolic Execution for JavaScript
PACMPL, vol. 3( POPL)
Skeletal Semantics and their Interpretations
PACMPL, vol. 3( POPL)
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
JaVerT: JavaScript Verification and Testing Framework: Invited Talk
Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 1:1–1:4