Termination Analysis with Compositional Transition Invariants

TitleTermination Analysis with Compositional Transition Invariants
Publication TypeConference Paper
Year of Publication2010
AuthorsKroening, D., Sharygina Natasha, Tsitovich A., and Wintersteiger C.M.
Conference NameInternational Conference on Computer-Aided Verification (CAV)
Conference LocationEdinburgh, UK

Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate that our algorithm is often able to conclude termination by examining only a small fraction of the program. As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude. 

Full Text