Dr Byron Cook, Microsoft Research and Queen Mary University of London
Proving the 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.
Date: Wednesday 4th November 2009
Venue: Royal Society, London SW1Y 5AG
Time: Registration 6.30pm, lecture starts at 7.00pm
For more information and how to book please visit: Roger Needham Lecture 2009
