Verified Trustworthy Software Specification

Prof Philippa Gardner

Department of Computing, Imperial College London

My ambitious goal, with others, is to bring rigorous, scientific method to the specification of modern software systems, in line with standard engineering practice. My research advocates for formal software specifications that are: validated, with proper evidence that they describe what they should; useful, identifying compositional building blocks that enable scalable client reasoning; and just right, in that implementation details should not leak into the specification statement and the specification should be at the same level of abstraction as the client. This talk describes some of my work on the specification of languages, libraries and programs, determining what it means for a specification to be appropriate for the task at hand, properly evaluated and useful for real-world applications. In particular, I will describe my work on WasmCert, a mechanised specification of the WebAssembly language in the Coq and Isabelle theorem provers, and Gillian, a multi-language platform for compositional testing, specification and verification of programs, instantiated to the real-world languages JavaScript and C. I will place this research in the wider context of projects funded by the Research Institute on Verified Trustworthy Software Systems (VeTSS) in particular, and current international research in general.

About Prof Philippa Gardner

Philippa Gardner is a Professor in the Department of Computing at Imperial College London and and has a UKRI Established Fellowship on `Verified Trustworthy Software Specification’, 2018–2023. Her current research focusses on program testing, specification and verification: in particular, on Coq-mechanised specifications of Javascript and WebAssembly (Wasm), on the Gillian multi-language platform for building compositional symbolic testing and verification tools for e.g. JavaScript and C, and on concurrent separation logics for reasoning compositionally about complex concurrent algorithms.Gardner completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial. Philippa is currently the Director of the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, and became a Fellow of the Royal Academy of Engineering in 2020.

Sponsored by

Official Media Partners

Supported by