Stephan Falke and Deepak Kapur:
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
In Proceedings of the 22nd International Conference on Automated Deduction (CADE '09), Montréal, Canada.
Lecture Notes in Artificial Intelligence 5663, pages 277-293, 2009. ©Springer-Verlag
An approach based on term rewriting techniques for the automated termination
analysis of imperative programs operating on integers is presented. An
imperative program 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)
|
Paper on SpringerLink
]