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)
]