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-2008-03
Proving Termination of Imperative Programs via Term Rewriting
Stephan Falke and Deepak Kapur
This paper adapts techniques from the term rewriting literature in order to show termination of imperative programs operating on numbers. For this, we present a two-stage approach. In the first stage, imperative programs are translated into constrained term rewrite systems operating on numbers, where constraints are quantifier-free formulas of Presburger arithmetic. This way, computations of imperative programs are mimicked by rewrite sequences. In the second stage, termination of constrained term rewrite systems is analyzed by specializing and simplifying the dependency pair framework for normalized equational rewriting with constraints. This approach is highly flexible and allows the use of various termination techniques adapted from the term rewriting literature, including graph-based decompositions and polynomial interpretations. The approach has been used to prove termination of a large collection of imperative programs.
News & Events | People | Academics | Research | Jobs | Companies | Visitors | Computer Facilities | Home
