tr-announce

Download

tr-announce@lists.rwth-aachen.de

February 2007

1 participants
2 discussions

2007-03: Proving Termination by Bounded Increase
by Peter Schneider-Kamp 23 Feb '07

23 Feb '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: Proving Termination by Bounded Increase Jürgen Giesl, René Thiemann, Stephan Swiderski, and Peter Schneider-Kamp AIB 2007-03 Most methods and tools for termination analysis of term rewrite systems (TRSs) essentially try to find arguments of functions that decrease in recursive calls. However, they fail if the reason for termination is that an argument is increased in recursive calls repeatedly until it reaches a bound. In this paper, we solve that problem and present a method to prove termination of TRSs with bounded increase automatically.

1 0

2007-02: SAT Solving for Termination Analysis with Polynomial Interpretations
by Peter Schneider-Kamp 07 Feb '07

07 Feb '07

The following technical report is available from http://aib.informatik.rwth-aachen.de: SAT Solving for Termination Analysis with Polynomial Interpretations Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl AIB 2007-02 Polynomial interpretations are one of the most popular techniques for automated termination analysis. Therefore, the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.

1 0