Loop Summarization and Termination Analysis

  • Aliaksei Tsitovich ,
  • Natasha Sharygina ,
  • Christoph M. Wintersteiger ,
  • Daniel Kroening

Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |

Published by Springer Verlag

Publication

We present a technique for program termination analysis based on loop summarization. The algorithm relies on a library of abstract domains to discover well-founded transition invariants. In contrast to state-of-the-art methods it aims to construct a complete ranking argument for all paths through a loop at once, thus avoiding expensive enumeration of individual paths. Compositionality is used as a completeness criterion for the discovered transition invariants. The practical efficiency of the approach is evaluated using a set of Windows device drivers.