UNM Computer Science

Search Technical Reports by ID



The format of the tech reports ID number is TR-CS-YYYY-NN, where YYYY is the four digit year and NN is the number, including leading zeroes. For the first tech report of 2004, the search would be "TR-CS-2004-01".

This searches only by ID. If you'd like, you can also search by researcher or search by keyword

Found 1 result.

Listing from newest to oldest



TR-CS-2009-02

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Stephan Falke and Deepak Kapur

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.

PDF