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é ThiemannJournal of Automated Reasoning, 58(1), pp. 3 – 31, 2017.
Abstract
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.
BibTeX
@article{AProVE-JAR17,
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},
}