Proving That Programs Eventually Do Something Good


July 2, 2013


Byron Cook




Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing), and those that result in the software not doing something useful (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. But, 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 this recent work and its application to industrial software.


Byron Cook

Dr. Byron Cook is a principal researcher at Microsoft’s laboratory at Cambridge University and full professor of computer science at Queen Mary, University of London. Byron’s research interests include program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. Byron’s recent work has been focused on the development of automatic tools for proving properties of biological models, Termination and liveness proving (the TERMINATOR project), and methods for discovering invariants regarding mutable data structures (the SLAyer project). Before joining MSR Byron was a dev lead in the Windows Base OS group on the SDV project. For more information about Dr. Cook, see


  • Portrait of Byron Cook

    Byron Cook