Analyzing Program Termination and Complexity Automatically with AProVE

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

Publikováno v: 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, vol. 58, no. 1, pp. 3-31 . https://doi.org/10.1007/s10817-016-9388-y

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 contai

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::20ed30e232c853f8e57d105104d9844a
https://findresearcher.sdu.dk:8443/ws/files/141379108/Analyzing_Program_Termination_and_Complexity_Automatically_with_AProVE.pdf

Analyzing runtime and size complexity of integer programs

Autor: Carsten Fuhs, Fabian Emmes, Stephan Falke, Marc Brockschmidt, Jürgen Giesl

We present a modular approach to automatic complexity analysis of integer programs. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer bounds on the absolute values of program variables, we ca

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0b366b89336b6454cf5a813b78307207
https://eprints.bbk.ac.uk/id/eprint/16257/1/16257.pdf

Alternating runtime and size complexity analysis of integer programs

Autor: Stephan Falke, Marc Brockschmidt, Jürgen Giesl, Carsten Fuhs, Fabian Emmes

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642548611
TACAS

We present a modular approach to automatic complexity analysis. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer size bounds on program variables, we can restrict each analysis step to a sma

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::14e7d43c694af88048391a2bb65f6408
https://eprints.bbk.ac.uk/id/eprint/16256/1/16256.pdf

Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs

Autor: Jürgen Giesl, Carsten Fuhs, Fabian Emmes, Thomas Ströder, Peter Schneider-Kamp

Publikováno v: Giesl, J, Ströder, T, Schneider-Kamp, P, Emmes, F & Fuhs, C 2013, Symbolic Evaluation Graphs and Term Rewriting — A General Methodology for Analyzing Logic Programs . in E Albert (ed.), Logic-Based Program Synthesis and Transformation . vol. 7844, Springer, Lecture Notes in Computer Science, vol. 7844, 22nd International Symposium on Logic-Based Program Synthesis and Transformation, Leuven, Belgium, 18/09/2012 . https://doi.org/10.1007/978-3-642-38197-3_1
LOPSTR
Giesl, J, Ströder, T, Schneider-Kamp, P, Emmes, F & Fuhs, C 2012, Symbolic Evaluation Graphs and Term Rewriting-A General Methodology for Analyzing Logic Programs . in Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12) . Association for Computing Machinery, 14th sSmposium on Principles and Practice of Declarative Programming, Leuven, Belgium, 19/09/2012 . https://doi.org/10.1145/2370776.2370778

There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of d

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ff9e0b22aac89e48b2fcdf2a7a75908c
https://portal.findresearcher.sdu.dk/da/publications/c0e865e7-2fff-4bbd-978b-6b5d3cca91b7

A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog

Autor: Carsten Fuhs, Fabian Emmes, Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder

Publikováno v: Logic-Based Program Synthesis and Transformation ISBN: 9783642322105
LOPSTR

We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including "non-logical" concepts like cuts, meta-programming, "all solution" predicates, dynamic predicates, and exception handling). In

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::a780c73bcd402e1bed3b1c2c9351225b
https://doi.org/10.1007/978-3-642-32211-2_16