Stephan Falke and Deepak Kapur:
Proving Termination of Imperative Programs via Term Rewriting
Technical Report TR-CS-2008-03, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2008.
This paper adapts techniques from the term rewriting literature in order to show termination of imperative programs operating on numbers. For this, we present a two-stage approach. In the first stage, imperative programs are translated into constrained term rewrite systems operating on numbers, where constraints are quantifier-free formulas of Presburger arithmetic. This way, computations of imperative programs are mimicked by rewrite sequences. In the second stage, termination of constrained term rewrite systems is analyzed by specializing and simplifying the dependency pair framework for normalized equational rewriting with constraints. This approach is highly flexible and allows the use of various termination techniques adapted from the term rewriting literature, including graph-based decompositions and polynomial interpretations. The approach has been used to prove termination of a large collection of imperative programs.
[ BibTeX | Paper (ps.gz) | Paper (pdf) ]