Analyzing Program Termination and Complexity Automatically with AProVE

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

Journal of Automated Reasoning, 58(1), pp. 3 – 31, 2017.


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


  PDF |    doi:10.1007/s10817-016-9388-y  


author = {J{\"{u}}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and
Florian Frohn and Carsten Fuhs and Jera Hensel 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 = {Analyzing Program Termination and Complexity Automatically with {AProVE}},
journal = {Journal of Automated Reasoning},
volume = {58},
number = {1},
pages = {3--31},
year = {2017},
doi = {10.1007/s10817-016-9388-y},
Nach oben scrollen