Abstract
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.
This work has been funded by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
Chapter PDF
Similar content being viewed by others
References
Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis (2005), arXiv:cs/0512056 [cs.MS]
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Acceleration from theory to practice. STTT 10(5), 401–424 (2008).https://doi.org/10.1007/s10009-008-0064-3
Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATVA ’05. pp. 474–488. LNCS 3707 (2005).https://doi.org/10.1007/11562948_35
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. Ph.D. thesis, Université de Liège (1999), https://orbi.uliege.be/bitstream/2268/74874/1/Boigelot98.pdf
Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science 309(1-3), 413–468 (2003). https://doi.org/10.1016/S0304-3975(03)00314-1
Bozga, M., Gîrlea, C., Iosif, R.: Iterating octagons. In: TACAS ’09. pp.337–351. LNCS 5505 (2009). https://doi.org/10.1007/978-3-642-00768-2_29
Bozga, M., Iosif, R., Konecný, F.: Fast acceleration of ultimately periodic relations. In: CAV ’10. pp. 227–242. LNCS 6174 (2010).https://doi.org/10.1007/978-3-642-14295-6_23
Bozga, M., Iosif, R., Konecný, F.: Deciding conditional termination. Logical Methods in Computer Science 10(3) (2014). https://doi.org/10.2168/LMCS-10(3:8)2014
Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: CAV ’98. pp. 268–279. LNCS 1427 (1998). https://doi.org/10.1007/BFb0028751
Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD ’15. pp.57–64 (2015). https://doi.org/10.1109/FMCAD.2015.7542253
Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: FMCAD ’19. pp. 221–230 (2019). https://doi.org/10.23919/FMCAD.2019.8894271
Frohn, F.: A calculus for modular loop acceleration – artifact evaluation(2020). https://doi.org/10.5281/zenodo.3676348
Frohn, F.: A calculus for modular loop acceleration (2020), extended version, arXiv:2001.01516 [cs.LO]
Frohn, F.: Empirical evaluation of “A calculus for modular loopacceleration” (2020), https://ffrohn.github.io/acceleration-calculus
Frohn, F., Hark, M., Giesl, J.: On the decidability of termination for polynomial loops (2019), arXiv:1910.11588 [cs.LO]
Frohn, F., Naaf, M., Brockschmidt, M., Giesl, J.: Inferring lower runtime bounds for integer programs (2019), arXiv:1911.01077 [cs.LO]
Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: IJCAR ’16. pp. 550–567. LNCS 9706 (2016). https://doi.org/10.1007/978-3-319-40229-1_37
Ganty, P., Iosif, R., Konecný, F.: Underapproximation of procedure summaries for integer programs. STTT 19(5), 565–584 (2017). https://doi.org/10.1007/s10009-016-0420-7
Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: TACAS ’19. pp. 156–166. LNCS 11429 (2019). https://doi.org/10.1007/978-3-030-17502-3_10
Gonnord, L., Halbwachs, N.: Combining widening and acceleration in line arrelation analysis. In: SAS ’06. pp. 144–160. LNCS 4134 (2006). https://doi.org/10.1007/11823230_10
Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Science of Computer Programming 93, 125–153 (2014). https://doi.org/10.1016/j.scico.2013.09.016
Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: POPL ’08. pp. 147–158 (2008). https://doi.org/10.1145/1328438.1328459
Hojjat, H., Iosif, R., Konecný, F., Kuncak, V., Rümmer, P.:Accelerating interpolants. In: ATVA ’12. pp. 187–202. LNCS 7561 (2012). https://doi.org/10.1007/978-3-642-33386-6_16
Hojjat, H., Konecný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems - tool paper. In: FM ’12. pp. 247–251. LNCS 7436 (2012). https://doi.org/10.1007/978-3-642-32759-9_21
Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL ’14. pp. 529–540 (2014). https://doi.org/10.1145/2535838.2535843
Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI ’17. pp. 248–262 (2017). https://doi.org/10.1145/3062341.3062373
Konecný, F.: PTIME computation of transitive closures of octagonal relations. In: TACAS ’16. pp. 645–661. LNCS 9636 (2016). https://doi.org/10.1007/978-3-662-49674-9_42
Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. FMSD 47(1),75–92 (2015). https://doi.org/10.1007/s10703-015-0228-1
Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: FMCAD ’15. pp. 105–111 (2015). https://doi.org/10.1109/FMCAD.2015.7542259
Mourade Moura, L., Bjørner, N.: An efficient SMT solver. In: TACAS ’08. pp. 337–340. LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: SODA ’15. pp. 957–969 (2015). https://doi.org/10.1137/1.9781611973730.65
Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: CAV ’19. pp. 97–115. LNCS 11562 (2019). https://doi.org/10.1007/978-3-030-25543-5_7
Strejcek, J., Trtík, M.: Abstracting path conditions. In: ISSTA ’12. pp.155–165 (2012). https://doi.org/10.1145/2338965.2336772
Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: IJCAR ’14. pp. 367–373. LNCS 8562(2014). https://doi.org/10.1007/978-3-319-08587-6_28
Termination problems data base (TPDB), http://termination-portal.org/wiki/TPDB
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Frohn, F. (2020). A Calculus for Modular Loop Acceleration. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)