Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs

Stephan Falke20 Contact Information and Deepak Kapur20 Contact Information

(20)  CS Department, University of New Mexico, Albuquerque, NM, USA
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.
Partially supported by NSF grants CCF-0541315 and CNS-0831462.

Contact Information Stephan Falke
Email: spf@cs.unm.edu

Contact Information Deepak Kapur
Email: kapur@cs.unm.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.81 • Server: mpweb05
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)