Automatically proving the termination of C programs

Опубликовано 6 сентября 2016, 6:00

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.