Automatically proving the termination of C programs


October 3, 2005


Byron Cook


Researcher, Microsoft Research, Cambridge


In this talk I will discuss Terminator, the first known automatic program termination proven to support large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. Additionally, to increase the proof power, Terminator computes inductive invariants of the program when checking the lemmas that imply termination. The talk will close with results from recent experiments with Terminator on dispatch routines from Windows device drivers. This is joint work with Andreas Podelski and Andrey Rybalchenko.


Byron Cook

Dr. Byron Cook is researcher at Microsoft’s laboratory at Cambridge University. He is also a visiting professor at Chalmers University and at Queen Mary, University of London. Byron’s research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Byron has recently been working on automatic tools for proving program termination and tools for proving properties about data structures. Byron is one of the developers behind the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. Byron’s PhD is from OGI.For more information about Dr. Cook, see


  • Portrait of Byron Cook

    Byron Cook