The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Skip to content



Automatically proving the termination of C programs

Cook, B (Microsoft Research)
Friday 03 February 2006, 11:00-12:00

Seminar Room 1, Newton Institute


In this talk I will discuss Terminator, which is a program termination prover that supports 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. The termination argument is constructed incrementally, based on failed proof attempts. Terminator also infers and proves required program invariants on demand. The lecture will close with information about the results of some experiments with Terminator on Windows device drivers.


MP3MP3 Real AudioReal Audio

Back to top ∧