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…