In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy.

Xavier Leroy discusses achieving extreme software reliability through formal verification tools that mathematically prove the absence of bugs.

2016 Milner Award lecture by Dr Xavier Leroy, a senior research scientist at Inria where he leads the Gallium research team. 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. The lecture was recorded on November 24 2016 at the Royal Society. For more events like this, see our schedule - ow.ly/KhTi306gTN1