Stephan Falke and Deepak Kapur:
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Technical Report TR-CS-2009-02, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2009.
An approach based on term rewriting techniques for the automated termination
analysis of imperative programs operating on integers is presented. An
imperative programs is transformed into rewrite rules with constraints from
quantifier-free Presburger arithmetic. Any computation in the imperative
program corresponds to a rewrite sequence, and termination of the rewrite
system thus implies termination of the imperative program. Termination of
the rewrite system is analyzed using a decision procedure for Presburger
arithmetic that identifies possible chains of rewrite rules, and
automatically generated polynomial interpretations are used to show
finiteness of such chains. An implementation of the approach has been
evaluated on a large collection of imperative programs, thus demonstrating
its effectiveness and practicality.
[
BibTeX
|
Paper (ps.gz)
|
Paper (pdf)
]