Personal tools
You are here: Home Events Abstract Archives 2006-2007 Automatically proving the termination of C programs

Automatically proving the termination of C programs

Byron Cook Microsoft Research, Cambridge 4pm Tuesday, March 21st 2006 Room 2511, JCMB, King's Buildings

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.

We are now using Terminator to prove that Windows device driver dispatch routines always return back to their calling context. This talk will close with some discussion on these experimental results together with a bit of information on recent extensions.

Dr Byron Cook is a researcher at Microsoft's laboratory at Cambridge University. Byron's research interests include program verification, model checking, automatic theorem proving, and programming language theory. Byron has recently been working on methods of proving program termination, decision procedures, counterexample-guided abstraction refinement for concurrent programs, and tools for proving properties about programs that modify the heap. Byron is one of the researchers who developed the SLAM software model checker, which is used in Microsoft's Static Driver Verifier product.

Document Actions