{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:49:35Z","timestamp":1761965375399,"version":"3.40.5"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031171079"},{"type":"electronic","value":"9783031171086"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"vor","delay-in-days":273,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Loop abstraction is a central technique for program analysis, because loops can cause large state-space representations if they are unfolded. In many cases, simple tricks can accelerate the program analysis significantly. There are several successful techniques for loop abstraction, but they are hard-wired into different tools and therefore difficult to compare and experiment with. We present a framework that allows us to implement different loop abstractions in one common environment, where each technique can be freely switched on and off on-the-fly during the analysis. We treat loops as part of the abstract model of the program, and use counterexample-guided abstraction refinement to increase the precision of the analysis by dynamically activating particular techniques for loop abstraction. The framework is independent from the underlying abstract domain of the program analysis, and can therefore be used for several different program analyses. Furthermore, our framework offers a sound transformation of the input program to a modified, more abstract output program, which is unsafe if the input program is unsafe. This allows loop abstraction to be used by other verifiers and our improvements are not \u2018locked in\u2019 to our verifier. We implemented several existing approaches and evaluate their effects on the program analysis.<\/jats:p>","DOI":"10.1007\/978-3-031-17108-6_1","type":"book-chapter","created":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T13:04:15Z","timestamp":1663765455000},"page":"3-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Unifying Approach for Control-Flow-Based Loop Abstraction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8172-3184","authenticated-orcid":false,"given":"Marian","family":"Lingsch Rosenfeld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9169-9130","authenticated-orcid":false,"given":"Martin","family":"Spiessl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: Verification by abstraction and test generation. In: Proc. ASE. pp. 1138\u20131141 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. PLDI. pp. 203\u2013213. ACM (2001). https:\/\/doi.org\/10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS (2). pp. 375\u2013402. LNCS 13244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"1_CR4","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5831003","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2022 and Test-Comp 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5831003","journal-title":"Zenodo"},{"issue":"3","key":"1_CR5","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/s10817-017-9432-6","volume":"60","author":"D Beyer","year":"2017","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299\u2013335 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","journal-title":"J. Autom. Reasoning"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Handbook of Model Checking, pp. 493\u2013540. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"issue":"5\u20136","key":"1_CR7","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 505\u2013525 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE. pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"1_CR9","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD. pp. 189\u2013197. FMCAD (2010)"},{"key":"1_CR10","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6793834","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Lingsch Rosenfeld, M., Spiessl, M.: Reproduction package for SEFM 2022 article \u2018A unifying approach for control-flow-based loop abstraction\u2019. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.6793834","journal-title":"Zenodo"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE. pp. 146\u2013162. LNCS 7793, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"issue":"1","key":"1_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. pp. 193\u2013207. LNCS 1579, Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"5","key":"1_CR14","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: Proc. DATE. pp. 1407\u20131412. IEEE (2015). https:\/\/doi.org\/10.7873\/DATE.2015.0245","DOI":"10.7873\/DATE.2015.0245"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Darke, P., Khanzode, M., Nair, A., Shrotri, U., Venkatesh, R.: Precise analysis of large industry code. In: Proc. APSEC. pp. 306\u2013309. IEEE (2012). https:\/\/doi.org\/10.1109\/APSEC.2012.97","DOI":"10.1109\/APSEC.2012.97"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Proc. TACAS (1). pp. 58\u201376. LNCS 12078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV. pp. 72\u201383. LNCS 1254, Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proc. POPL. pp. 529\u2013540. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535843","DOI":"10.1145\/2535838.2535843"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Handbook of Model Checking, pp. 447\u2013491. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proc. POPL. pp. 194\u2013206. ACM (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Proc. TACAS (1). pp. 213\u2013231. LNCS 10805, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_12","DOI":"10.1007\/978-3-319-89960-2_12"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Madhukar, K., Wachter, B., Kr\u00f6ning, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: Proc. FMCAD. pp. 105\u2013111. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"1_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999). https:\/\/doi.org\/10.1007\/978-3-662-03811-6","journal-title":"Principles of Program Analysis. Springer"},{"issue":"3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Proc. CAV, Part 2. pp. 97\u2013115. LNCS 11562, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17108-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T17:05:39Z","timestamp":1710867939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17108-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031171079","9783031171086"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17108-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The software and programs that we used for our experiments, including the generated programs with abstracted loops, are open source and available on our supplementary web page at  and in the reproduction package at Zenodo\u00a0[].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"value":"This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) \u2013  (ConVeY).","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding Statement"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Berlin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"49% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}