Termination Analysis with Compositional Transition Invariants

Keywords:

Abstract:

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. 

• BibTex

@inproceedings { KSTW10,
	title = {Termination Analysis with  Compositional Transition Invariants},
	booktitle = {International Conference on Computer-Aided Verification (CAV)},
	year = {2010},
	pages = {89-103},
	publisher = {Springer},
	organization = {Springer},
	address = {Edinburgh, UK},
	keywords = {Termination, transition invariants},
	URL = {http://dx.doi.org/10.1007/978-3-642-14295-6_9},
	author = {Daniel Kroening and  Natasha Sharygina and   Aliaksei Tsitovich and   Christoph M. Wintersteiger}
}