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, Stephanie Swiderski, and René Thiemann

Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Lecture Notes in Computer Science 8562, pp. 184 – 191, 2014.


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.


  PDF |    doi:10.1007/978-3-319-08587-6_13  |  © Springer International Publishing Switzerland


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"
Nach oben scrollen