Skip to content

In search of software perfection

Prize lecture

Event video


18:30 - 19:30


The Royal Society, London, 6-9 Carlton House Terrace, London, SW1Y 5AG


Dr Xavier Leroy, Inria

2016 Milner Award lecture by Dr Xavier Leroy.

Xavier Leroy is a senior research scientist at Inria where he leads the Gallium research team. His research focuses on programming languages and tools, and on the formal verification of software using program proof and static analysis. He is the architect and one of the main developers of the OCaml functional programming language and of the CompCert formally-verified C compiler.

In the general public, "software" has become synonymous with "crashes" and "security holes".  Yet, there exists life-critical software systems that achieve extraordinary levels of reliability.  For example, fly-by-wire systems, involving considerable amounts of software, have been used in commercial airplanes for nearly 40 years without any incident caused by a software bug.  

What does it take to achieve this kind of software perfection?  This lecture will describe some of the approaches involved, with special emphasis on the use of formal verification tools - that is, programs that check other programs for the absence of whole classes of bugs.  These tools provide highly valuable guarantees that complement, and sometimes subsume, the assurance obtained by more traditional techniques such as testing.  Beware however: a bug in the verification tool or in the compiler that produce the actual executable from verified sources could ruin these guarantees.  How can we rule out this risk?  Using the CompCert verified C compiler as an example, the lecture will discuss a radical, mathematically-grounded answer: the formal verification, using proof assistants, of the tools that participate in the construction and verification of critical software.

Attending the event

  • Free to attend
  • No registration required
  • Doors open from 18:00, and seats are allocated on a first-come, first-served basis 
  • British Sign Language interpretation and live subtitles are available upon request

The award

The Royal Society Milner Award, supported by Microsoft Research, is given annually for outstanding achievement in computer science by a European researcher.

It replaces the Royal Society and Académie des sciences Microsoft Award and is named in honour of Professor Robin Milner FRS (1934-2010), a pioneer in computer science.

The winner of the award receives a medal and a personal prize of £5,000. The winner is invited to deliver a public lecture on their research at the Society

For all enquiries, please contact the Events Team.

In search of software perfection The Royal Society, London 6-9 Carlton House Terrace London SW1Y 5AG UK