Links to external sources may no longer work as intended. The content may not represent the latest thinking in this area or the Society’s current position on the topic.
In search of software perfection
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.