Paper Info
Title
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Abstract
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.
Year
DOI
Venue
2009
10.1007/978-3-642-02959-2_22
CADE
Keywords
Field
DocType
possible chain,automated termination analysis,decision procedure,imperative program,quantifier-free presburger arithmetic,term rewriting approach,large collection,imperative program corresponds,imperative programs,presburger arithmetic,polynomial interpretation,termination analysis
Integer,Discrete mathematics,Programming language,Polynomial,Computer science,Algorithm,Disjunctive normal form,Presburger arithmetic,Termination analysis,Rewriting,Computation
Conference
Volume
ISSN
Citations 
5663
0302-9743
10
PageRank 
References 
Authors
0.67
20
2
Name
Order
Citations
PageRank
Stephan Falke151127.86
Deepak Kapur22282235.00