{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:42Z","timestamp":1777348002027,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911200","type":"print"},{"value":"9783031911217","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>\n          <jats:p>Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked\u00a0data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis\u2019 precision. We extend the underlying symbolic execution and propose a framework for <jats:italic>shared abduction<\/jats:italic> where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose <jats:italic>biabductive loop acceleration<\/jats:italic>, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called <jats:italic>shape extrapolation<\/jats:italic>. This heuristic takes advantage of locality in the handling of list-like\u00a0data structures (which are the most common data structures found in low-level\u00a0code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also\u00a0make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase\u00a0can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques;\u00a0both in terms of precision and runtime of the analysis.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_10","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:07:18Z","timestamp":1746187638000},"page":"230-257","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5839-0726","authenticated-orcid":false,"given":"Florian","family":"Sextl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7911-0549","authenticated-orcid":false,"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2746-8792","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS. pp. 97\u2013109. LNCS, Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_9","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: Biere, A., Parker, D. (eds.) TACAS. pp. 347\u2013367. LNCS, Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_21","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS. pp. 299\u2013329. LNCS, Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. pp. 459\u2013465. LNCS, Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_33","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. SIGPLAN Not. 44(1), 289\u2013300 (2009). https:\/\/doi.org\/10.1145\/1594834.1480917","DOI":"10.1145\/1594834.1480917"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6) (2011). https:\/\/doi.org\/10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS. pp. 366\u2013378 (2007). https:\/\/doi.org\/10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS. pp. 287\u2013302. LNCS, Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_19","DOI":"10.1007\/11691372_19"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Dr\u0103goi, C., Enea, C., Sighireanu, M.: Local shape analysis for overlaid data structures. In: SAS. pp. 150\u2013171. LNCS, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_10","DOI":"10.1007\/978-3-642-38856-9_10"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS. pp. 215\u2013237. LNCS, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_13","DOI":"10.1007\/978-3-642-38856-9_13"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Giet, J., Ridoux, F., Rival, X.: A product of shape and sequence abstractions. In: Hermenegildo, M.V., Morales, J.F. (eds.) SAS. pp. 310\u2013342. LNCS, Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_15","DOI":"10.1007\/978-3-031-44245-2_15"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis. In: Palsberg, J., Su, Z. (eds.) SAS. pp. 188\u2013204. LNCS, Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_14","DOI":"10.1007\/978-3-642-03237-0_14"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Peringer, P., Rogalewicz, A., \u0160okov\u00e1, V., Vojnar, T., Zuleger, F.: Low-Level Bi-Abduction. In: Ali, K., Vitek, J. (eds.) ECOOP. LIPIcs, vol.\u00a0222, pp. 19:1\u201319:30. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.19","DOI":"10.4230\/LIPIcs.ECOOP.2022.19"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NASA Formal Methods. pp. 212\u2013229. LNCS, Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_15","DOI":"10.1007\/978-3-319-57288-8_15"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Illous, H., Lemerre, M., Rival, X.: Interprocedural shape analysis using separation logic-based transformer summaries. In: Pichardie, D., Sighireanu, M. (eds.) SAS. pp. 248\u2013273. LNCS, Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65474-0_12","DOI":"10.1007\/978-3-030-65474-0_12"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Kaindlstorfer, D.: Enhancing Abstraction and Symbolic Execution for Shape Analysis of C-Programs operating on Linked Lists. Diploma thesis, TU Wien (2023). https:\/\/doi.org\/10.34726\/hss.2023.109623","DOI":"10.34726\/hss.2023.109623"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV. pp. 52\u201368. LNCS, Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_4","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O\u2019Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527325","DOI":"10.1145\/3527325"},{"key":"10_CR19","unstructured":"Magill, S., Nanevski, A., Clarke, E.M., Lee, P.: Inferring invariants in separation logic for imperative list-processing programs (2015), draft"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Maksimovi\u0107, P., Cronj\u00e4ger, C., L\u00f6\u00f6w, A., Sutherland, J., Gardner, P.: Exact separation logic: Towards bridging the gap between verification and bug-finding. In: Ali, K., Salvaneschi, G. (eds.) ECOOP. LIPIcs, vol.\u00a0263, pp. 19:1\u201319:27. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2023.19","DOI":"10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Sergey, I.: Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290385","DOI":"10.1145\/3290385"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Qin, S., He, G., Chin, W.N., Craciun, F., He, M., Ming, Z.: Automated specification inference in a combined domain via user-defined predicates. Sci. Comput. Program. 148(C), 189\u2013212 (2017). https:\/\/doi.org\/10.1016\/j.scico.2017.05.007","DOI":"10.1016\/j.scico.2017.05.007"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Raad, A., Berdine, J., Dang, H.H., Dreyer, D., O\u2019Hearn, P., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: CAV. pp. 225\u2013252. LNCS, Springer, Berlin, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_14","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Raad, A., Berdine, J., Dreyer, D., O\u2019Hearn, P.W.: Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498695","DOI":"10.1145\/3498695"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55\u201374. IEEE Computer Society, USA (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Rysavy, L.: Join operators for bi-abductive analysis of low-level code. Diploma thesis, TU Wien (2024). https:\/\/doi.org\/10.34726\/hss.2024.119373","DOI":"10.34726\/hss.2024.119373"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Sammler, M., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., Garg, D.: RefinedC: automating the foundational verification of c code with refined ownership types. In: PLDI. pp. 158\u2013174. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Sextl, F., Rogalewicz, A., Vojnar, T., Zuleger, F.: Artifact for \"compositional shape analysis with shared abduction and biabductive loop acceleration\" (2025). https:\/\/doi.org\/10.5281\/zenodo.14623977","DOI":"10.5281\/zenodo.14623977"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Sextl, F., Rogalewicz, A., Vojnar, T., Zuleger, F.: Compositional shape analysis with shared abduction and biabductive loop acceleration (Extended Version) (2024), https:\/\/arxiv.org\/abs\/2307.06346","DOI":"10.1007\/978-3-031-91121-7_10"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Spies, S., G\u00e4her, L., Sammler, M., Dreyer, D.: Quiver: Guided abductive inference of separation logic specifications in coq. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656413","DOI":"10.1145\/3656413"},{"key":"10_CR31","unstructured":"Wyatt, P.: Avoiding game crashes related to linked lists (2012), http:\/\/www.codeofhonor.com\/blog\/avoiding-game-crashes-related-to-linked-lists"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Zilberstein, N., Dreyer, D., Silva, A.: Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proc. ACM Program. Lang. 7(OOPSLA1) (2023). https:\/\/doi.org\/10.1145\/3586045","DOI":"10.1145\/3586045"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Zilberstein, N., Saliling, A., Silva, A.: Outcome separation logic: Local reasoning for correctness and incorrectness with computational effects. Proc. ACM Program. Lang. 8(OOPSLA1) (2024). https:\/\/doi.org\/10.1145\/3649821","DOI":"10.1145\/3649821"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:43:23Z","timestamp":1746521003000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"The proof-of-concept implementation of our techniques, called Brushin the text, is available as an artifact [].","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Code Availability"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}