For decades, computer scientists have dreamt of using machine-assisted reasoning to bring the rigor of scientific and mathematical methods to the specification and verification of software systems, a vision proposed by Turing, Hoare, and Milner. Today, this dream is edging closer to reality: proof assistants have matured; verification tools are increasingly tractable; and real-world software is now being formally specified and verified both in academia and industry. Recent advances in mathematical techniques and well-engineered tools have made it possible to reason about large, open industrial systems at scale.

In this talk, I will give a whirl-wind tour of recent progress – by myself and others – on the formal specification and verification of language standards, libraries and general-purpose programs. I will discuss what it means for a specification to be appropriate, well-evaluated and useful for real-world applications. Topics will include the mechanised specification of the W3C WebAssembly language standard through a new process called Wasm SpecTec; compositional software analysis techniques and tools based on separation logic (SL), that enable the independent specification of functions within large, open, industrial codebases; and, briefly, compositional techniques for the verified specification of complex shared-memory concurrent programs.

Despite the considerable progress achieved, much still remains to be done to bring scientific, mathematical methods to the specification and verification of our modern software systems.

Philippa Gardner is a professor in the Department of Computing at Imperial College London and and has a UKRI Established Fellowship from 2018–2023. Her current research focusses on program verification: in particular, reasoning about Web programs (JavaScript and DOM); and reasoning about concurrent programs. She 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 directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC, from 2017 to 2022. She chaired the BCS awards committee, 2013-2018, which decides the Lovelace medal (senior) and Roger Needham award (mid-career) for computer science and engineering.