×

Analyzing program termination and complexity automatically with AProVE. (English) Zbl 1409.68255

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N15 Theory of programming languages
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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)
[2] 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) · Zbl 1306.68017
[3] Alpuente, M., Escobar, S., Lucas, S.: Removing redundant arguments automatically. TPLP 7(1-2), 3-35 (2007) · Zbl 1112.68068
[4] AProVE. http://aprove.informatik.rwth-aachen.de/
[5] Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, The University of Iowa. http://smt-lib.org/ (2015) · Zbl 1314.68174
[6] Bertot, Y., Castéran, P.: Coq’Art. Springer, Berlin (2004) · Zbl 1069.68095
[7] 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) · Zbl 1223.68101 · doi:10.1017/S0960129511000120
[8] Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: CAV ’05, pp. 491-504 (2005) · Zbl 1081.68611
[9] Bray, T.: The JavaScript object notation (JSON) data interchange format. (2014). RFC 7159 · Zbl 1222.68064
[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) · Zbl 1236.68036
[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) · Zbl 1139.68049
[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) · Zbl 1243.68267
[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) · doi:10.1145/2866575
[15] Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: SPIN ’12, pp. 248-254 (2012) · Zbl 1112.68068
[16] Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semiring constraints (extended abstract). In: SMT ’12, pp. 87-96 (2012) · Zbl 1243.68267
[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) · Zbl 1276.68140 · doi:10.1007/s10817-010-9211-0
[18] Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: RTA ’11, pp. 21-30 (2011) · Zbl 1236.68219
[19] Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS ’13, pp. 47-61 (2013) · Zbl 1381.68050
[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) · Zbl 1223.68101
[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) · Zbl 1276.68140
[23] Eclipse. http://www.eclipse.org/
[24] Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT ’03, pp. 502-518 (2004) · Zbl 1204.68191
[25] Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: IJCAR ’12, pp. 225-240 (2012) · Zbl 1358.68157
[26] Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2-3), 195-220 (2008) · Zbl 1139.68049 · doi:10.1007/s10817-007-9087-9
[27] Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA ’11, pp. 41-50 (2011) · Zbl 1236.68040
[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) · Zbl 1366.68116
[29] Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: IJCAR ’16, pp. 550-567 (2016) · Zbl 1475.68134
[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) · Zbl 1214.68352
[31] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: RTA ’08, pp. 110-125 (2008) · Zbl 1145.68446
[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) · Zbl 1166.68354
[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) · Zbl 1242.68131
[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) · Zbl 1243.68267 · doi:10.1007/s10817-010-9215-9
[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) · Zbl 1171.68714
[37] Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. JAR 37(3), 155-203 (2006) · Zbl 1113.68088 · doi:10.1007/s10817-006-9057-7
[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) · Zbl 1213.68347
[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) · doi:10.1145/1890028.1890030
[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) · Zbl 06208064
[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) · Zbl 1409.68256
[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) · Zbl 1390.68181
[44] Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357-392 (2009) · Zbl 1224.68041
[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) · Zbl 1188.68196
[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) · Zbl 1222.68064
[50] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002) · Zbl 0994.68131
[51] Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. JAR 51(1), 27-56 (2013) · Zbl 1314.68174 · doi:10.1007/s10817-013-9277-6
[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) · Zbl 1236.68145
[53] Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI ’04, pp. 239-251 (2004) · Zbl 1202.68109
[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) · doi:10.1145/1709093.1709095
[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) · Zbl 1326.68063
[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) · Zbl 1423.68110
[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) · Zbl 1186.68076 · doi:10.1007/s10601-008-9061-0
[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) · Zbl 1252.68265
[64] Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173-201 (2009) · Zbl 1184.68303 · doi:10.1007/s10817-009-9131-z
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.