Byron Cook: Automatically Proving the Termination of C Programs

Categories: Event

Byron Cook is a researcher at Microsoft’s research lab at Cambridge University:

In this talk I will discuss Terminator, the first known automatic program termination prover 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.

For more information about the speaker, see


Friday, October 7, 2005 - 10:00 to 11:00


ICICS/CS Board Room (288)



When: to

Where: ICICS/CS Board Room (288) - 2366 Main Mall, Vancouver, BC, V6T 1Z4

Add to my calendar