Abstract

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.

BibTeX

@inproceedings{APROVE-IJCAR14,
  author      = "J{\"u}rgen Giesl and Marc Brockschmidt and Fabian Emmes
                 and Florian Frohn and Carsten Fuhs and Carsten Otto and
                 Martin Pl{\"u}cker and Peter Schneider-Kamp and
                 Thomas Str{\"o}der and Stephanie Swiderski and Ren{\'e}
                 Thiemann",
  title       = "Proving Termination of Programs Automatically with
                 {AProVE}",
  booktitle   = "Proceedings of the 7th International Joint Conference on
                 Automated Reasoning",
  editor      = "St{\'e}phane Demri and Deepak Kapur and Christoph
                 Weidenbach",
  series      = "Lecture Notes in Computer Science",
  volume      = 8562,
  pages       = "184--191",
  year        = 2014,
  doi         = "10.1007/978-3-319-08587-6_13"
}