Title | Termination Analysis with Compositional Transition Invariants |
Publication Type | Conference Paper |
Year of Publication | 2010 |
Authors | Kroening, D., Sharygina Natasha, Tsitovich A., and Wintersteiger C.M. |
Conference Name | International Conference on Computer-Aided Verification (CAV) |
Publisher | Springer |
Conference Location | Edinburgh, UK |
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. |
Full Text |