{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T03:41:04Z","timestamp":1782358864429,"version":"3.54.5"},"publisher-location":"Cham","reference-count":36,"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><jats:italic>Bounded Model Checking<\/jats:italic> (BMC) is a powerful technique for proving unsafety. However, finding <jats:italic>deep counterexamples<\/jats:italic> that require a large bound is challenging for BMC. On the other hand, <jats:italic>acceleration techniques<\/jats:italic> compute \u201cshortcuts\u201d\u00a0that \u201ccompress\u201d many execution steps into a single one. In this paper, we tightly integrate acceleration techniques into SMT-based bounded model checking. By adding suitable \u201cshortcuts\u201d on the fly, our approach can quickly detect deep counterexamples. Moreover, using so-called <jats:italic>blocking clauses<\/jats:italic>, our approach can prove safety of examples where BMC diverges. An empirical comparison with other state-of-the-art techniques shows that our approach is highly competitive for proving unsafety, and orthogonal to existing techniques for proving safety.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_4","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"73-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Integrating Loop Acceleration Into Bounded Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Artifact for \u201cIntegrating Loop Acceleration into Bounded Model Checking\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.11954015","DOI":"10.5281\/zenodo.11954015"},{"key":"4_CR2","unstructured":"Evaluation of \u201cIntegrating Loop Acceleration into Bounded Model Checking\u201d (2024). https:\/\/loat-developers.github.io\/abmc-eval\/"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: Solidity compiler\u2019s model checker. In: CAV 2022. LNCS, vol. 13371, pp. 325\u2013338. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"issue":"5","key":"4_CR4","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S Bardin","year":"2008","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","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A.: Bounded model checking. In: Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 739\u2013764. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201002","DOI":"10.3233\/FAIA201002"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: TACAS\u00a02022. LNCS, vol. 13243, pp. 524\u2013542. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: TACAS 2009. LNCS, vol. 5505, pp. 337\u2013351. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_29","DOI":"10.1007\/978-3-642-00768-2_29"},{"key":"4_CR9","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Relational analysis of integer programs. Technical Report TR-2012-10, VERIMAG (2012). https:\/\/www-verimag.imag.fr\/TR\/TR-2012-10.pdf"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Calzavara, S., Grishchenko, I., Maffei, M.: HornDroid: practical and sound static analysis of Android applications by SMT solving. In: EuroS &P\u00a02016, pp. 47\u201362. IEEE (2016). https:\/\/doi.org\/10.1109\/EuroSP.2016.16","DOI":"10.1109\/EuroSP.2016.16"},{"key":"4_CR11","unstructured":"CHC Competition. https:\/\/chc-comp.github.io"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"De Angelis, E., Govind V. K., H.: CHC-COMP 2023: Competition report (2023). https:\/\/chc-comp.github.io\/2023\/CHC_COMP_2023_Competition_Report.pdf","DOI":"10.4204\/EPTCS.402.10"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Ultimate TreeAutomizer (CHC-COMP tool description). In: HCVS\/PERR@ETAPS 2019. EPTCS, vol. 296, pp. 42\u201347 (2019). https:\/\/doi.org\/10.4204\/EPTCS.296.7","DOI":"10.4204\/EPTCS.296.7"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: CAV\u00a02014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"4_CR15","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Ernst, G.: Loop verification with invariants and contracts. In: VMCAI\u00a02022 [2], pp. 69\u201392 (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_4","DOI":"10.1007\/978-3-030-94583-1_4"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained Horn clauses using syntax and data. In: FMCAD\u00a02018 [1], pp.\u00a01\u20139 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603011","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: TACAS\u00a02020. LNCS, vol. 12078, pp. 58\u201376. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Frohn, F., Naaf, M., Brockschmidt, M., Giesl, J.: Inferring lower runtime bounds for integer programs. ACM Trans. Program. Lang. Syst. 42(3), 13:1\u201313:50 (2020). https:\/\/doi.org\/10.1145\/3410331","DOI":"10.1145\/3410331"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: IJCAR\u00a02022. LNCS, vol. 13385, pp. 712\u2013722. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination by acceleration driven clause learning. In: CADE\u00a02023. LNCS, vol. 14132, pp. 220\u2013233. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_13","DOI":"10.1007\/978-3-031-38499-8_13"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: ADCL: Acceleration driven clause learning for constrained Horn clauses. In: SAS\u00a02023. LNCS, vol. 14284, pp. 259\u2013285. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_13","DOI":"10.1007\/978-3-031-44245-2_13"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Integrating loop acceleration into bounded model checking. CoRR abs\/2401.09973 (2024). https:\/\/doi.org\/10.48550\/arXiv.2401.09973","DOI":"10.48550\/arXiv.2401.09973"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CAV\u00a02015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Hoder, K., Bj\u00f8rner, N.S.: Generalized property directed reachability. In: SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: ATVA\u00a02012. LNCS, vol. 7561, pp. 187\u2013202. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_16","DOI":"10.1007\/978-3-642-33386-6_16"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The Eldarica Horn solver. In: FMCAD\u00a02018 [1], pp.\u00a01\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: JayHorn: a framework for verifying Java programs. In: CAV\u00a02016. LNCS, vol. 9779, pp. 352\u2013358. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"issue":"3","key":"4_CR29","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"4_CR30","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s10703-015-0228-1","volume":"47","author":"D Kroening","year":"2015","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. Formal Methods Syst. Des. 47(1), 75\u201392 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0228-1","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Proving safety with trace automata and bounded model checking. In: FM\u00a02015. LNCS, vol. 9109, pp. 325\u2013341. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_21","DOI":"10.1007\/978-3-319-19249-9_21"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. ACM Trans. Program. Lang. Syst. 43(4), 15:1\u201315:54 (2021). https:\/\/doi.org\/10.1145\/3462205","DOI":"10.1145\/3462205"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS 2008. LNCS, vol. 4963, 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":"4_CR34","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: IJCAR\u00a02014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., W\u00fcstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartACE. In: VMCAI\u00a02022 [2], pp. 425\u2013449. https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","DOI":"10.1007\/978-3-030-94583-1_21"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: PLDI 2018, pp. 707\u2013721 (2018). https:\/\/doi.org\/10.1145\/3192366.3192416","DOI":"10.1145\/3192366.3192416"}],"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_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:03:01Z","timestamp":1725933781000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_4","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"}}]}}