{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:53:37Z","timestamp":1777305217016,"version":"3.51.4"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","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,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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>Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools.<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_3","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:46:06Z","timestamp":1753130766000},"page":"56-80","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Arithmetizing Shape Analysis"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Wolff","sequence":"first","affiliation":[]},{"given":"Ekanshdeep","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Zafer","family":"Esen","sequence":"additional","affiliation":[]},{"given":"Hossein","family":"Hojjat","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"3_CR1","unstructured":"c\/memsafety-broom benchmark suite of SV-COMP 2024. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/tree\/svcomp24-final\/c\/memsafety-broom. Accessed 04 Aug 2025"},{"key":"3_CR2","unstructured":"Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Ji, R., Rezine, A.: Shape analysis via monotonic abstraction. In: Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, vol. 08171. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany (2008)"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Baier, D., et al.: CPACHECKER 2.3 with strategy selection - (competition contribution). In: Finkbeiner, B., Kovacs, L. (eds) TACAS (3). Lecture Notes in Computer Science, vol. 14572, pp. 359\u2013364. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_21","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Balakrishnan, G., Reps, T.W.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04134, pp. 221\u2013239. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11823230_15","DOI":"10.1007\/11823230_15"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2007","unstructured":"Berdine, J., et al.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178\u2013192. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_22"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, S.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds) CAV. Lecture Notes in Computer Science, vol.\u00a05123, pp. 399\u2013413. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_37","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kovacs, L. (eds) TACAS (3). Lecture Notes in Computer Science, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: SV-benchmarks: benchmark set for software verification (SV-COMP 2024) (version svcomp24) (2024). https:\/\/doi.org\/10.5281\/ZENODO.10669723","DOI":"10.5281\/ZENODO.10669723"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lemberger, T.: CPA-SymExec: efficient symbolic execution in CPACHECKER. In: ASE, pp. 900\u2013903. ACM (2018)","DOI":"10.1145\/3238147.3240478"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-14295-6_8","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2010","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Rezine, A., Sighireanu, M.: Invariant synthesis for programs manipulating lists with unbounded data. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 72\u201388. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_8"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2011","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.) NFM 2011. LNCS, vol. 6617, pp. 459\u2013465. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_33"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289\u2013300. ACM (2009)","DOI":"10.1145\/1480881.1480917"},{"issue":"1\u20132","key":"3_CR13","first-page":"1","volume":"6","author":"BE Chang","year":"2020","unstructured":"Chang, B.E., Dragoi, C., Manevich, R., Rinetzky, N., Rival, X.: Shape analysis. Found. Trends Program. Lang. 6(1\u20132), 1\u2013158 (2020)","journal-title":"Found. Trends Program. Lang."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_24"},{"key":"3_CR16","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. Lecture Notes in Computer Science, vol.\u00a03920, pp. 287\u2013302. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_19","DOI":"10.1007\/11691372_19"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds) CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 372\u2013378. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_29","DOI":"10.1007\/978-3-642-22110-1_29"},{"key":"3_CR18","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. Lecture Notes in Computer Science, vol.\u00a07935, pp. 215\u2013237. 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":"3_CR19","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2\u201315. ACM (2009)","DOI":"10.1145\/1480881.1480885"},{"key":"3_CR20","unstructured":"Esen, Z., R\u00fcmmer, P.: Tricera: Verifying C programs using the theory of heaps. In: FMCAD, pp. 380\u2013391. IEEE (2022)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213\u2013224. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_14"},{"key":"3_CR22","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. Lecture Notes in Computer Science, vol. 14284, pp. 310\u2013342. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_15","DOI":"10.1007\/978-3-031-44245-2_15"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C. (eds) CAV (1). Lecture Notes in Computer Science, vol.\u00a09206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-21668-3_26","volume-title":"Computer Aided Verification","author":"C Hawblitzel","year":"2015","unstructured":"Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 449\u2013465. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_26"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-662-49122-5_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Haziza","year":"2016","unstructured":"Haziza, F., Hol\u00edk, L., Meyer, R., Wolff, S.: Pointer race freedom. In: Jobstmann, B., Leino, K. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 393\u2013412. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_19"},{"key":"3_CR26","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-49727-7_4","volume-title":"Static Analysis","author":"M Hind","year":"1998","unstructured":"Hind, M., Pioli, A.: Assessing the effects of flow-sensitivity on pointer alias analyses. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 57\u201381. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49727-7_4"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-32759-9_21","volume-title":"FM 2012: Formal Methods","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Kone\u010dn\u00fd, F., Garnier, F., Iosif, R., Kuncak, V., R\u00fcmmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247\u2013251. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_21"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: FMCAD, pp.\u00a01\u20137. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Kotoun, M., Peringer, P., Sokov\u00e1, V., Trt\u00edk, M., Vojnar, T.: Predator shape analysis tool suite. In: Haifa Verification Conference. Lecture Notes in Computer Science, vol. 10028, pp. 202\u2013209 (2016)","DOI":"10.1007\/978-3-319-49052-6_13"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/978-3-642-39799-8_52","volume-title":"Computer Aided Verification","author":"L Hol\u00edk","year":"2013","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 740\u2013755. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_52"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Meyer, R., Vojnar, T., Wolff, S.: Effect summaries for thread-modular analysis. CoRR abs\/1705.03701 (2017)","DOI":"10.1007\/978-3-319-66706-5_9"},{"key":"3_CR33","unstructured":"Hol\u00edk, L., Peringer, P., Rogalewicz, A., Sokov\u00e1, V., Vojnar, T., Zuleger, F.: Low-level bi-abduction. In: ECOOP. LIPIcs, vol.\u00a0222, pp. 19:1\u201319:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"issue":"3","key":"3_CR34","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/s10703-021-00366-4","volume":"57","author":"H Illous","year":"2021","unstructured":"Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. Formal Methods Syst. Des. 57(3), 343\u2013400 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756\u2013772. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_53"},{"issue":"4","key":"3_CR36","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of lisp-like structures. In: POPL, pp. 244\u2013256. ACM Press (1979)","DOI":"10.1145\/567752.567776"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Kersten, R., R\u00fcmmer, P., Sch\u00e4f, M.: Quantified heap invariants for object-oriented programs. In: LPAR. EPiC Series in Computing, vol.\u00a046, pp. 368\u2013384. EasyChair (2017)","DOI":"10.29007\/zrct"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-96145-3_5","volume-title":"Computer Aided Verification","author":"B Kragl","year":"2018","unstructured":"Kragl, B., Qadeer, S.: Layered concurrent programs. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 79\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_5"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Krishna, S., Patel, N., Shasha, D.E., Wies, T.: Verifying concurrent search structure templates. In: PLDI, pp. 181\u2013196. ACM (2020)","DOI":"10.1145\/3385412.3386029"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Krishna, S., Shasha, D.E., Wies, T.: Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang. 2(POPL), 37:1\u201337:31 (2018)","DOI":"10.1145\/3158125"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-030-44914-8_12","volume-title":"Programming Languages and Systems","author":"S Krishna","year":"2020","unstructured":"Krishna, S., Summers, A.J., Wies, T.: Local reasoning for global graph properties. In: ESOP 2020. LNCS, vol. 12075, pp. 308\u2013335. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_12"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL, pp. 171\u2013182. ACM (2008)","DOI":"10.1145\/1328438.1328461"},{"issue":"12","key":"3_CR45","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL, pp. 123\u2013136. ACM (2012)","DOI":"10.1145\/2103656.2103673"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Meyer, R., Opaterny, A., Wies, T., Wolff, S.: nekton: a linearizability proof checker. In: CAV (1). Lecture Notes in Computer Science, vol. 13964, pp. 170\u2013183. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_9","DOI":"10.1007\/978-3-031-37706-8_9"},{"issue":"OOPSLA2","key":"3_CR48","doi-asserted-by":"publisher","first-page":"1378","DOI":"10.1145\/3563337","volume":"6","author":"R Meyer","year":"2022","unstructured":"Meyer, R., Wies, T., Wolff, S.: A concurrent program logic with a future and history. Proc. ACM Program. Lang. 6(OOPSLA2), 1378\u20131407 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Meyer, R., Wies, T., Wolff, S.: Embedding hindsight reasoning in separation logic. Proc. ACM Program. Lang. 7(PLDI), 1848\u20131871 (2023)","DOI":"10.1145\/3591296"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Meyer, R., Wies, T., Wolff, S.: Make flows small again: revisiting the flow framework. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 628\u2013646. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_32","DOI":"10.1007\/978-3-031-30823-9_32"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Meyer, R., Wolff, S.: Decoupling lock-free data structures from memory reclamation for static analysis. Proc. ACM Program. Lang. 3(POPL), 58:1\u201358:31 (2019)","DOI":"10.1145\/3290371"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Meyer, R., Wolff, S.: Pointer life cycle types for lock-free data structures with memory reclamation. Proc. ACM Program. Lang. 4(POPL), 68:1\u201368:36 (2020)","DOI":"10.1145\/3371136"},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-662-46681-0_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Muller","year":"2015","unstructured":"Muller, P., Peringer, P., Vojnar, T.: Predator hunting party (Competition Contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 443\u2013446. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_40"},{"key":"3_CR54","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (eds) CSL. Lecture Notes in Computer Science, vol.\u00a02142, pp. 1\u201319. Springer, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"3_CR55","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Peringer, P., Sokov\u00e1, V., Vojnar, T.: Predatorhp revamped (not only) for interval-sized memory regions and memory reallocation (competition contribution). In: Biere, A., Parker, D. (eds) TACAS (2). Lecture Notes in Computer Science, vol. 12079, pp. 408\u2013412. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_30","DOI":"10.1007\/978-3-030-45237-7_30"},{"key":"3_CR57","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) Static Analysis, pp. 268\u2013283. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_19"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"3_CR59","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., 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":"3_CR60","doi-asserted-by":"publisher","unstructured":"Sextl, F., Rogalewicz, A., Vojnar, T., Zuleger, F.: Compositional shape analysis with shared abduction and biabductive loop acceleration. In: Vafeiadis, V. (eds) Programming Languages and Systems - 34th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-91121-7_10","DOI":"10.1007\/978-3-031-91121-7_10"},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Boehm, H., Jr., G.L.S. (eds.) Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pp. 32\u201341. ACM Press (1996). https:\/\/doi.org\/10.1145\/237721.237727","DOI":"10.1145\/237721.237727"},{"key":"3_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375\u2013395. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_23"},{"key":"3_CR63","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008)"},{"key":"3_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450\u2013464. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40"},{"key":"3_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256\u2013271. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_18"},{"key":"3_CR66","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., W\u00fcstholz, V., Gurfinkel, A.: Inductive predicate synthesis modulo programs. In: ECOOP. LIPIcs, vol.\u00a0313, pp. 43:1\u201343:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"3_CR67","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T Wies","year":"2011","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 476\u2013491. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_36"},{"key":"3_CR68","doi-asserted-by":"publisher","unstructured":"Wolff, S., Gupta, E., Esen, Z., Hojjat, H., R\u00fcmmer, P., Wies, T.: Arithmetizing shape analysis. CoRR abs\/2408.09037 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2408.09037","DOI":"10.48550\/ARXIV.2408.09037"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98668-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:13:08Z","timestamp":1777302788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_3","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":"22 July 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":"Disclaimers"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}