{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:42:59Z","timestamp":1768005779305,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A wide variety of algorithms is employed for the reachability analysis of programs with loops but most of them are restricted to single loop programs. Recently a new technique called Transition Power Abstraction (TPA) showed promising results for safety checks of software. In contrast to many other techniques TPA efficiently handles loops with a large number of iterations. This paper introduces an algorithm that enables the effective use of TPA for analysis of multiloop programs. The TPA-enabled loop analysis reduces the dependency on the number of possible iterations. Our approach analyses loops in a modular manner and both computes and uses transition invariants incrementally, making program analysis efficient. The new algorithm is implemented in the Golem solver. Conducted experiments demonstrate that this approach outperforms the previous implementation of TPA and other competing tools on a wide range of multiloop benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_29","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"558-576","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reachability Analysis for\u00a0Multiloop Programs Using Transition Power Abstraction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7843-7290","authenticated-orcid":false,"given":"Konstantin","family":"Britikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8140-4098","authenticated-orcid":false,"given":"Martin","family":"Blicha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8872-4913","authenticated-orcid":false,"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"29_CR1","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science\/World Student Series Edition. Addison-Wesley (1986). https:\/\/www.worldcat.org\/oclc\/12285707"},{"key":"29_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"29_CR3","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401\u2013424 (2008). https:\/\/doi.org\/10.1007\/s10009-008-0064-3","DOI":"10.1007\/s10009-008-0064-3"},{"key":"29_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 495\u2013522. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"29_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Second competition on software verification - (summary of SV-COMP 2013). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 594\u2013609. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_43","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"29_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, Austin, pp. 25\u201332. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351147","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"29_CR7","unstructured":"Beyer, D., Lee, N., Wendler, P.: Interpolation and sat-based model checking revisited: adoption to software verification. arXiv preprint arXiv:2208.05046 (2022)"},{"key":"29_CR8","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The golem horn solver. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 209\u2013223. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"29_CR9","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Split transition power abstraction for unbounded safety. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, pp. 349\u2013358. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_42","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_42"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 524\u2013542. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"29_CR11","doi-asserted-by":"publisher","unstructured":"Blicha, M., Kofron, J., Tatarko, W.: Summarization of branching loops. In: Hong, J., Bures, M., Park, J.W., Cern\u00fd, T. (eds.) The 37th ACM\/SIGAPP Symposium on Applied Computing, Virtual Event (SAC 2022), 25\u201329 April 2022, pp. 1808\u20131816. ACM (2022). https:\/\/doi.org\/10.1145\/3477314.3507042","DOI":"10.1145\/3477314.3507042"},{"key":"29_CR12","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P.B. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"29_CR13","unstructured":"Bueno, D.: Horn2vmt: Translating horn reachability into transition systems. Tech. rep., Sandia National Lab.(SNL-NM), Albuquerque, NM (United States) (2020)"},{"issue":"3","key":"29_CR14","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbol. Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symbol. Logic"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: Nebel, W., Atienza, D. (eds.) Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, DATE 2015, Grenoble, pp. 1407\u20131412. ACM (2015). http:\/\/dl.acm.org\/citation.cfm?id=2757139","DOI":"10.7873\/DATE.2015.0245"},{"key":"29_CR16","doi-asserted-by":"publisher","unstructured":"Darke, P., Khanzode, M., Nair, A., Shrotri, U., Venkatesh, R.: Precise analysis of large industry code. In: Leung, K.R.P.H., Muenchaisri, P. (eds.) 19th Asia-Pacific Software Engineering Conference, APSEC 2012, Hong Kong, 4\u20137 December 2012, pp. 306\u2013309. IEEE (2012). https:\/\/doi.org\/10.1109\/APSEC.2012.97","DOI":"10.1109\/APSEC.2012.97"},{"key":"29_CR17","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des. 39(1), 83\u2013113 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0124-2","DOI":"10.1007\/s10703-011-0124-2"},{"key":"29_CR18","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Kaufman, S.J., Bod\u00edk, R.: Learning inductive invariants by sampling from frequency distributions. Formal Methods Syst. Des. 56(1), 154\u2013177 (2020). https:\/\/doi.org\/10.1007\/s10703-020-00349-x","DOI":"10.1007\/s10703-020-00349-x"},{"key":"29_CR19","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 58\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. arXiv preprint arXiv:1905.11187 (2019)","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"29_CR21","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Dwyer, M.B., Tip, F. (eds.) Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, pp. 23\u201333. ACM (2011). https:\/\/doi.org\/10.1145\/2001420.2001424","DOI":"10.1145\/2001420.2001424"},{"key":"29_CR22","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, pp. 232\u2013244. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"29_CR23","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) Formal Methods in Computer Aided Design, FMCAD 2018, Austin, pp.\u00a01\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"29_CR24","doi-asserted-by":"publisher","unstructured":"Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying horn clauses using abstract interpretation and finite tree automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol.\u00a09779, pp. 261\u2013268. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_14","DOI":"10.1007\/978-3-319-41528-4_14"},{"key":"29_CR25","unstructured":"Kamath, A., et al.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)"},{"key":"29_CR26","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","DOI":"10.1007\/s10703-016-0249-4"},{"key":"29_CR27","doi-asserted-by":"publisher","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 111\u2013125. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_10","DOI":"10.1007\/978-3-540-88387-6_10"},{"key":"29_CR28","doi-asserted-by":"publisher","unstructured":"Lin, S., Sun, J., Xiao, H., Liu, Y., San\u00e1n, D., Hansen, H.: Fib: squeezing loop invariants by interpolation between forward\/backward predicate transformers. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, pp. 793\u2013803. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115690","DOI":"10.1109\/ASE.2017.8115690"},{"key":"29_CR29","unstructured":"McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical report. MSR-TR-2013-6 (2013)"},{"key":"29_CR30","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Jr., W.A.H., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Cham (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"29_CR31","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"29_CR32","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"29_CR33","unstructured":"Nielson, H.R., Nielson, F.: Semantics with applications - a formal introduction. In: Wiley Professional Computing. Wiley (1992)"},{"key":"29_CR34","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: CLN2INV: learning loop invariants with continuous logic networks. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia. OpenReview.net (2020). https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"29_CR35","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 97\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"29_CR36","doi-asserted-by":"publisher","unstructured":"Strejcek, J., Trt\u00edk, M.: Abstracting path conditions. In: Heimdahl, M.P.E., Su, Z. (eds.) International Symposium on Software Testing and Analysis, ISSTA 2012, Minneapolis, pp. 155\u2013165. ACM (2012). https:\/\/doi.org\/10.1145\/2338965.2336772","DOI":"10.1145\/2338965.2336772"},{"key":"29_CR37","doi-asserted-by":"publisher","unstructured":"Xie, X., Chen, B., Zou, L., Liu, Y., Le, W., Li, X.: Automatic loop summarization via path dependency analysis. IEEE Trans. Software Eng. 45(6), 537\u2013557 (2019). https:\/\/doi.org\/10.1109\/TSE.2017.2788018","DOI":"10.1109\/TSE.2017.2788018"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:08:07Z","timestamp":1725934087000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}