Proving termination through conditional termination. (English) Zbl 1452.68046
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 99-117 (2017).
Summary: We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine conditional termination proofs. Our key insight is that a conditional termination proof shows termination for a subset of program execution states which do not need to be considered in the remaining analysis. This facilitates more effective termination as well as non-termination analyses, and allows handling loops with different execution phases naturally. Moreover, our method can deal with sequences of loops compositionally. In an empirical evaluation, we show that our implementation VeryMax outperforms state-of-the-art tools on a range of standard benchmarks.
For the entire collection see [Zbl 1360.68015].
For the entire collection see [Zbl 1360.68015].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Barthe, G., Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2-18. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68863-1_2 · doi:10.1007/978-3-540-68863-1_2 |
| [2] | Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117-133. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_8 · Zbl 1306.68017 · doi:10.1007/978-3-642-15769-1_8 |
| [3] | Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. IC 215, 47-67 (2012) · Zbl 1251.68073 |
| [4] | Bakhirkin, A., Piterman, N.: Finding recurrent sets with backward analysis and trace partitioning. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 17-35. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_2 · Zbl 1420.68063 · doi:10.1007/978-3-662-49674-9_2 |
| [5] | Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL (2013) · Zbl 1301.68153 |
| [6] | Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009) · Zbl 1183.68568 |
| [7] | Bozga, M., Iosif, R., Konecný, F.: Deciding conditional termination. LCMS 10(3), 1-61 (2014) · Zbl 1338.68047 |
| [8] | Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491-504. Springer, Heidelberg (2005). doi:10.1007/11513988_48 · Zbl 1081.68611 · doi:10.1007/11513988_48 |
| [9] | Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413-429. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_28 · doi:10.1007/978-3-642-39799-8_28 |
| [10] | Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387-393. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_22 · doi:10.1007/978-3-662-49674-9_22 |
| [11] | Brockschmidt, M., Joosten, S.J., Thiemann, R., Yamada, A.: Certifying safety and termination proofs for integer transition systems. In: WST (2016) · Zbl 1494.68294 |
| [12] | Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Compositional safety verification with Max-SMT. In: FMCAD (2015) |
| [13] | Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions, for JBC. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123-141. Springer, Heidelberg (2011). doi:10.1007/978-3-642-31762-0_9 · doi:10.1007/978-3-642-31762-0_9 |
| [14] | Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156-171. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_11 · doi:10.1007/978-3-642-54862-8_11 |
| [15] | Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328-340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_32 · Zbl 1155.68431 · doi:10.1007/978-3-540-70545-1_32 |
| [16] | Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006) · Zbl 1141.68365 |
| [17] | D’Silva, V., Urban, C.: Conflict-driven conditional termination. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 271-286. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_16 · Zbl 1381.68155 · doi:10.1007/978-3-319-21668-3_16 |
| [18] | Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA (2011) · Zbl 1236.68040 |
| [19] | Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 261-277. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27705-4_21 · doi:10.1007/978-3-642-27705-4_21 |
| [20] | Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275-295. Springer, Cham (2014). doi:10.1007/978-3-319-12736-1_15 · Zbl 1453.68047 · doi:10.1007/978-3-319-12736-1_15 |
| [21] | Ganty, P., Genaim, S.: Proving termination starting from the end. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 397-412. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_27 · doi:10.1007/978-3-642-39799-8_27 |
| [22] | 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.: Analyzing program termination and complexity automatically with AProVE. JAR (2016, to appear) · Zbl 1409.68255 |
| [23] | Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: PLDI (2015) |
| [24] | Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL (2008) · Zbl 1295.68158 |
| [25] | Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304-319. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_19 · Zbl 1306.68027 · doi:10.1007/978-3-642-15769-1_19 |
| [26] | Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797-813. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_53 · doi:10.1007/978-3-319-08867-9_53 |
| [27] | Kop, C., Nishida, N.: Constrained term rewriting tool. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 549-557. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_38 · Zbl 1471.68110 · doi:10.1007/978-3-662-48899-7_38 |
| [28] | Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89-103. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_9 · doi:10.1007/978-3-642-14295-6_9 |
| [29] | Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779-796. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_52 · doi:10.1007/978-3-319-08867-9_52 |
| [30] | Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: FMCAD (2013) |
| [31] | Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333-350. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_25 · Zbl 1423.68457 · doi:10.1007/978-3-319-09284-3_25 |
| [32] | Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: PLDI (2015) |
| [33] | Leike, J., Heizmann, M.: Ranking templates for linear loops. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 172-186. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_12 · Zbl 1391.68020 · doi:10.1007/978-3-642-54862-8_12 |
| [34] | Massé, D.: Policy iteration-based conditional termination and ranking functions. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 453-471. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_25 · Zbl 1428.68125 · doi:10.1007/978-3-642-54013-4_25 |
| [35] | Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239-251. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_20 · Zbl 1202.68109 · doi:10.1007/978-3-540-24622-0_20 |
| [36] | Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245-259. Springer, Heidelberg (2007). doi:10.1007/978-3-540-69611-7_16 · doi:10.1007/978-3-540-69611-7_16 |
| [37] | Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703-719. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_57 · doi:10.1007/978-3-642-22110-1_57 |
| [38] | Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745-761. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_50 · doi:10.1007/978-3-319-08867-9_50 |
| [39] | Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. TOPLAS 32(3), 8:1-8:70 (2010) · doi:10.1145/1709093.1709095 |
| [40] | Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367-373. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_28 · doi:10.1007/978-3-319-08587-6_28 |
| [41] | Termination Competition. http://termination-portal.org/wiki/Termination_Competition |
| [42] | Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81-95. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_9 · Zbl 1315.68106 · doi:10.1007/978-3-642-19835-9_9 |
| [43] | Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 43-62. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_5 · doi:10.1007/978-3-642-38856-9_5 |
| [44] | Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54-70. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_4 · doi:10.1007/978-3-662-49674-9_4 |
| [45] | Urban, C., Miné, A.: A decision tree abstract domain for proving conditional termination. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302-318. Springer, Cham (2014). doi:10.1007/978-3-319-10936-7_19 · doi:10.1007/978-3-319-10936-7_19 |
| [46] | Velroyen, H. · Zbl 1138.68460 · doi:10.1007/978-3-540-79124-9_11 |
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.
