Sciweavers

RTA
2004
Springer

Automated Termination Proofs with AProVE

14 years 3 months ago
Automated Termination Proofs with AProVE
We describe the system AProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient algorithms based on classical simplification orders, dependency pairs, and the size-change principle. In particular, it contains many new improvements of the dependency pair approach that make automated termination proving more powerful and efficient. In AProVE, termination proofs can be performed with a user-friendly graphical interface and the system is currently among the most powerful termination provers available.
Jürgen Giesl, René Thiemann, Peter Sch
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where RTA
Authors Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
Comments (0)