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

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

81 Downloads (Pure)

Resumé

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.

OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind58
Udgave nummer1
Sider (fra-til)3-31
ISSN0168-7433
DOI
StatusUdgivet - 2017

Fingeraftryk

High level languages
Software engineering

Citer dette

Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., ... Thiemann, R. (2017). Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning, 58(1), 3-31. https://doi.org/10.1007/s10817-016-9388-y
Giesl, Jürgen ; Aschermann, Cornelius ; Brockschmidt, Marc ; Emmes, Fabian ; Frohn, Florian ; Fuhs, Carsten ; Hensel, Jera ; Otto, Carsten ; Plücker, Martin ; Schneider-Kamp, Peter ; Ströder, Thomas ; Swiderski, Stephanie ; Thiemann, René. / Analyzing Program Termination and Complexity Automatically with AProVE. I: Journal of Automated Reasoning. 2017 ; Bind 58, Nr. 1. s. 3-31.
@article{aa819b684b0c420abd2a5a0e8518d56d,
title = "Analyzing Program Termination and Complexity Automatically with AProVE",
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.",
keywords = "Complexity analysis, Java/C/Haskell/Prolog programs, Term rewriting, Termination analysis",
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",
year = "2017",
doi = "10.1007/s10817-016-9388-y",
language = "English",
volume = "58",
pages = "3--31",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "1",

}

Giesl, J, Aschermann, C, Brockschmidt, M, Emmes, F, Frohn, F, Fuhs, C, Hensel, J, Otto, C, Plücker, M, Schneider-Kamp, P, Ströder, T, Swiderski, S & Thiemann, R 2017, 'Analyzing Program Termination and Complexity Automatically with AProVE', Journal of Automated Reasoning, bind 58, nr. 1, s. 3-31. https://doi.org/10.1007/s10817-016-9388-y

Analyzing Program Termination and Complexity Automatically with AProVE. / Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René.

I: Journal of Automated Reasoning, Bind 58, Nr. 1, 2017, s. 3-31.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Analyzing Program Termination and Complexity Automatically with AProVE

AU - Giesl, Jürgen

AU - Aschermann, Cornelius

AU - Brockschmidt, Marc

AU - Emmes, Fabian

AU - Frohn, Florian

AU - Fuhs, Carsten

AU - Hensel, Jera

AU - Otto, Carsten

AU - Plücker, Martin

AU - Schneider-Kamp, Peter

AU - Ströder, Thomas

AU - Swiderski, Stephanie

AU - Thiemann, René

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Complexity analysis

KW - Java/C/Haskell/Prolog programs

KW - Term rewriting

KW - Termination analysis

U2 - 10.1007/s10817-016-9388-y

DO - 10.1007/s10817-016-9388-y

M3 - Journal article

VL - 58

SP - 3

EP - 31

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1

ER -