Speaker: Dr. Byron Cook, Microsoft Research TITLE: Automatically Proving the Termination of C Programs DATE : Friday, Oct. 7th, 2005 TIME : 10:00-11:30 a.m. ROOM : ICICS/CS Board Room (288) HOST : Alan Hu ABSTRACT: 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. BIO: Byron Cook is a researcher at Microsoft's research lab at Cambridge University. Byron is interested in a variety of techniques for proving the correctness of programs. Together with Tom Ball, Vladimir Levin, Sriram Rajamani, and others, Byron developed the SLAM software model checker. This is now used in the Windows Static Driver Verifier product. Before joining Microsoft, Byron worked for Prover Technology where he developed SAT-based symbolic model checking tools. He did his PhD in programming language theory at OGI. For more information about the speaker, see: http://research.microsoft.com/~bycook/