Abstract:

In this talk I will discuss TERMINATOR, which is an automatic 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 that TERMINATOR finds 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.

Byron Cook is a researcher at Microsoft's laboratory at Cambridge University in England. Byron is also a visiting professor at Chalmers University and at Queen Mary, University of London. Byron's research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Byron has recently been working on a number of formal verification related tools, including TERMINATOR and SLAyer, Byron developed the SLAM software model checker together with Tom Ball, Vladimir Levin, Jakob Lichtenberg, Sriram Rajamani, and many others. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers.