Analyzing Program Termination and Complexity Automatically with AProVE

作者：Giesl Juergen^*; Aschermann Cornelius; Brockschmidt Marc; Emmes Fabian; Frohn Florian; Fuhs Carsten; Hensel Jera; Otto Carsten; Pluecker Martin; Schneider Kamp Peter; Stroeder Thomas; Swiderski Stephanie; Thiemann Rene

来源：Journal of Automated Reasoning, 2017, 58(1): 3-31.

DOI：10.1007/s10817-016-9388-y

• Termination analysis
• Complexity analysis
• Java/C/Haskell/Prolog programs
• Term rewriting

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.

• 出版日期2017-1