@inproceedings { 186, title = {Termination Analysis with Compositional Relations}, booktitle = {22nd International Conference on Computer Aided Verification}, volume = {6174}, year = {2010}, month = {15/07/2010}, pages = {89-103}, publisher = {Springer}, organization = {Springer}, address = {Edinburgh}, 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.

}, author = {Daniel Kroening and Natasha Sharygina and Aliaksei Tsitovich and Christoph Wintersteiger} }