Sciweavers

Share
CAV
2010
Springer

Termination Analysis with Compositional Transition Invariants

9 years 7 months ago
Termination Analysis with Compositional Transition Invariants
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.
Daniel Kroening, Natasha Sharygina, Aliaksei Tsito
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger
Comments (0)
books