Proving Termination of Programs Automatically with AProVE

  • Jürgen Giesl ,
  • Marc Brockschmidt ,
  • Fabian Emmes ,
  • Florian Frohn ,
  • Carsten Fuhs ,
  • Carsten Otto ,
  • Martin Plücker ,
  • Peter Schneider-Kamp ,
  • Thomas Ströder ,
  • Steffi Swiderski ,
  • René Thiemann

IJCAR |

Published by Springer

Download BibTex

AProVE is a system for automatic termination and complexity proofs of Java, C, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level languages, AProVE automatically converts them to TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting TRSs. The generated proofs can be exported to check their correctness using automatic certifiers. For use in software construction, we present an AProVE plug-in for the popular Eclipse software development environment.