The 2009 lecture was delivered by Dr Byron Cook, senior researcher at Microsoft's laboratory at Cambridge University and Professor of Computer Science at Queen Mary, University of London.
'Proving that programs eventually do something good'
Software failures can be sorted into two groups: those that cause the software to crash, and those that result in the software hanging. Although crashes are frustrating, we at least know that we must take drastic action (e.g. rebooting).
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 undecidablity, 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 this recent work and its application to industrial software.