@conference {154,
	title = {Termination Analysis with Compositional Transition Invariants},
	booktitle = {International Conference on Computer-Aided Verification (CAV)},
	year = {2010},
	publisher = {Springer},
	organization = {Springer},
	address = {Edinburgh, UK},
	abstract = {<p style="text-align: justify;"><span style="color: rgb(73, 73, 73); font-family: {\textquoteright}Lucida Grande{\textquoteright}, {\textquoteright}Bitstream Vera Sans{\textquoteright}, Arial, sans-serif; ">Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check\&nbsp;is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of\&nbsp;ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate\&nbsp;that our algorithm is often able to conclude termination by examining\&nbsp;only a small fraction of the program. As a consequence, our algorithm is\&nbsp;able to outperform known approaches by multiple orders of magnitude.\&nbsp;</span></p>
},
	author = {Kroening, D. and Natasha Sharygina and Tsitovich, A. and Wintersteiger, C.M.}
}
