Roger Needham lecture 2009

Proving that programs eventually do something good

Speaker: Dr Byron Cook, senior researcher at Microsoft's laboratory at Cambridge University, and Professor of Computer Science at Queen Mary University of London.

Software failures can be sorted into two groups: those that cause the software to crash, and those that result in the software to hang. Although crashes are frustrating, we at least know that we must take drastic action (e.g. rebooting), but hangs are psychologically more difficult, as there is always the lingering possibility that we are simply too impatient and should wait a while longer for the machine to respond.

In recent years, automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. Based on Alan Turing's proof of the halting problem's undecidability, many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe the recent work and its application to industrial software.