Automatically proving the termination of C programs

Speaker  Byron Cook

Affiliation  Researcher, Microsoft Research, Cambridge

Host  Tom Ball

Duration  01:05:45

Date recorded  3 October 2005

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.

©2005 Microsoft Corporation. All rights reserved.
> Automatically proving the termination of C programs