nach oben

Erschienen in:

21.10.2016

Analyzing Program Termination and Complexity Automatically with AProVE

verfasst von: 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

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Preface

Nächster Artikel Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

In our earlier papers, this was often called a termination graph.

While termination can be analyzed for Java, C, Haskell, Prolog, TRSs, and int-TRSs, the current version of AProVE analyzes complexity only for Prolog and TRSs. In addition, complexity of integer transition systems (a restriction of int-TRSs) is analyzed by calling the tools KoAT and LoAT.

An initial “ExampleProject ” with several examples in different programming languages can be created by clicking on the “AProVE ” entry in Eclipse’s menu bar.

In (C), TRSs are listed as “QDP” (dependency pair problems [37]) and int-TRSs are shown as “IRSwT” (“Integer Rewrite Systems with Terms”).

See http://www.termination-portal.org/wiki/Java_Bytecode for the conventions of the Termination Competition, which also contain a detailed discussion of the limitations imposed on analyzed Java programs.

Here, LLVM stands for the intermediate representation of the LLVM compilation framework [46]. To analyze C programs, they are first compiled to LLVM and analyzed afterwards. This is similar to our approach for Java where we consider Java Bytecode instead of Java source code.

In the Proof Tree View, we do not only have complexity icons like or for problems, but proof steps also result in complexities (e.g., or ). More precisely, in each proof step, a problem P is transformed into a new problem \(P'\) and a complexity c from the rewrite rule(s) whose contribution to P’s complexity is accounted for in this step. Then the complexity of P is bounded by the maximum (asymptotically equivalent to the sum) of \(P'\)’s complexity and c.

So our int-TRSs extend int -based TRSs from [27] by constructors and restrict integer TRSs (ITRSs) from [33] by not allowing nested defined symbols.

The nesting level of a variable x in a term \(t = f(t_1, \ldots , t_n)\) is \(\mathsf {nl}(t, x) = 1 + \max \{ \mathsf {nl}(t_i, x) \mid 1 \le i \le n, x \in {{\mathrm{\mathcal {V}}}}_{\mathcal {T\!A}}(t_i) \}\) if \(x \in {{\mathrm{\mathcal {V}}}}_{\mathcal {T\!A}}(t)\), where \(\mathsf {nl}(x,x) = 0\), and \(\mathsf {nl}(t, x) = \infty \) if \(x \notin {{\mathrm{\mathcal {V}}}}_{\mathcal {T\!A}}(t)\).

The results for the C benchmarks are similar.

So this concept of polynomial interpretations encompasses both polynomial ranking functions for defined function symbols and size measures/norms/abstractions for constructors of data structures.

See http://cl-informatik.uibk.ac.at/software/cpf/.

Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Removing useless variables in cost analysis of Java Bytecode. In: SAC ’08, pp. 368–375 (2008)

Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: SAS ’10, pp. 117–133 (2010)

Alpuente, M., Escobar, S., Lucas, S.: Removing redundant arguments automatically. TPLP 7(1–2), 3–35 (2007)MathSciNetMATH

AProVE. http://aprove.informatik.rwth-aachen.de/

Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, The University of Iowa. http://smt-lib.org/ (2015)

Bertot, Y., Castéran, P.: Coq’Art. Springer, Berlin (2004)MATH

Blanqui, F., Koprowski, A.: CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 4, 827–859 (2011)MathSciNetCrossRefMATH

Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: CAV ’05, pp. 491–504 (2005)

Bray, T.: The JavaScript object notation (JSON) data interchange format. (2014). RFC 7159

10.

Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: RTA ’11, pp. 155–170 (2011)

11.

Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: FoVeOOS ’11, pp. 123–141 (2012)

12.

Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: CAV ’12, pp. 105–122 (2012)

13.

Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: CAV ’13, pp. 413–429 (2013)

14.

Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM TOPLAS 38(4), 13:1–13:50 (2016)CrossRef

15.

Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: SPIN ’12, pp. 248–254 (2012)

16.

Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semiring constraints (extended abstract). In: SMT ’12, pp. 87–96 (2012)

17.

Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. JAR 49(1), 53–93 (2012)MathSciNetCrossRefMATH

18.

Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: RTA ’11, pp. 21–30 (2011)

19.

Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS ’13, pp. 47–61 (2013)

20.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL ’77, pp. 238–252 (1977)

21.

de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS ’08, pp. 337–340 (2008)

22.

Dutertre, B., de Moura, L.M.: The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper (2006)

23.

Eclipse. http://www.eclipse.org/

24.

Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT ’03, pp. 502–518 (2004)

25.

Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: IJCAR ’12, pp. 225–240 (2012)

26.

Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2–3), 195–220 (2008)MathSciNetCrossRefMATH

27.

Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA ’11, pp. 41–50 (2011)

28.

Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Ströder, T.: Inferring lower bounds for runtime complexity. In: RTA ’15, pp. 334–349 (2015)

29.

Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: IJCAR ’16, pp. 550–567 (2016)

30.

Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R.,Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: SAT ’07, pp. 340–354 (2007)

31.

Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: RTA ’08, pp. 110–125 (2008)

32.

Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: AISC ’08, pp. 109–124 (2008)

33.

Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: RTA ’09, pp. 32–47 (2009)

34.

Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dependency pairs and inductive theorem proving. JAR 47(2), 133–160 (2011)MathSciNetCrossRefMATH

35.

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: RTA ’04, pp. 210–220 (2004)

36.

Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: FroCoS ’05, pp. 216–231 (2005)

37.

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. JAR 37(3), 155–203 (2006)MathSciNetCrossRefMATH

38.

Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: IJCAR ’06, pp. 281–286 (2006)

39.

Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: CADE ’07, pp. 443–459 (2007)

40.

Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM TOPLAS 33(2), 7:1–7:39 (2011)CrossRef

41.

Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting—a general methodology for analyzing logic programs. In: PPDP ’12, pp. 1–12 (2012)

42.

Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: IJCAR ’14, pp. 184–191 (2014)

43.

Hensel, J., Giesl, J., Frohn, F., Ströder, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In SEFM ’16, pp. 234–252 (2016)

44.

Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357–392 (2009)MathSciNetMATH

45.

Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report Memo MTP-3, Louisiana Technical University (1979)

46.

Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO ’04, pp. 75–88 (2004)

47.

Le Berre, D., Parrain, A.: The SAT4J library, release 2.2. JSAT 7, 59–64 (2010)

48.

McMillan, K.: Lazy abstraction with interpolants. In: CAV ’06, pp. 123–136 (2006)

49.

Nguyen, M.T., De Schreye, D., Giesl, J., Schneider-Kamp, P.: Polytool: polynomial interpretations as a basis for termination analysis of logic programs. TPLP 11(1), 33–63 (2011)MathSciNetMATH

50.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)MATH

51.

Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. JAR 51(1), 27–56 (2013)MathSciNetCrossRefMATH

52.

Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In RTA ’10, pp. 259–276 (2010)

53.

Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI ’04, pp. 239–251 (2004)

54.

SMT-COMP. http://www.smt-comp.org/

55.

Spoto, F., Lunjin, L., Mesnard, F.: Using CLP simplifications to improve Java Bytecode termination analysis. ENTCS 253(5), 129–144 (2009)

56.

Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS 32(3), 8:1–8:70 (2010)CrossRef

57.

Ströder, T., Schneider-Kamp, P., Giesl, J.: Dependency triples for improving termination analysis of logic programs with cut. In: LOPSTR ’10, pp. 184–199 (2011)

58.

Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: IJCAR ’14, pp. 208–223 (2014)

59.

Ströder, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: termination and memory safety of C programs (competition contribution). In: TACAS ’15, pp. 417–419 (2015)

60.

SV-COMP. http://sv-comp.sosy-lab.org/

61.

Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254–272 (2009)MathSciNetCrossRefMATH

62.

Termination Comp. http://termination-portal.org/wiki/Termination_Competition

63.

Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs ’09, pp. 452–468 (2009)

64.

Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173–201 (2009)MathSciNetCrossRefMATH

Titel: Analyzing Program Termination and Complexity Automatically with AProVE
verfasst von: 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
Publikationsdatum: 21.10.2016
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-016-9388-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2017

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

Preface

The Bayesian Ontology Language

Solution Validation and Extraction for QBF Preprocessing

An Approximation Framework for Solvers and Decision Procedures

Soundness and Completeness Proofs by Coinductive Methods

Premium Partner