{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:19:34Z","timestamp":1781075974331,"version":"3.54.1"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"crossref","award":["200021-156980"],"award-info":[{"award-number":["200021-156980"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by first-order SMT solvers, which impedes automatic verification.<\/jats:p>\n          <jats:p>In this paper, we present a modular specification and verification technique for reachability properties in separation logic. For each method, we specify reachability only locally within the fragment of the heap on which the method operates. We identify relative convexity, a novel relation between the heap fragments of a client and a callee, which enables (first-order) reachability framing, that is, extending reachability properties from the heap fragment of a callee to the larger fragment of its client, enabling precise procedure-modular reasoning. Our technique supports practically important heap structures, namely acyclic graphs with a bounded outdegree as well as (potentially cyclic) graphs with at most one path (modulo cycles) between each pair of nodes. The integration into separation logic allows us to reason about reachability and other properties in a uniform way, to verify concurrent programs, and to automate our technique via existing separation logic verifiers. We demonstrate that our verification technique is amenable to SMT-based verification by encoding a number of benchmark examples into the Viper verification infrastructure.<\/jats:p>","DOI":"10.1145\/3360547","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Modular verification of heap reachability properties in separation logic"],"prefix":"10.1145","volume":"3","author":[{"given":"Arshavir","family":"Ter-Gabrielyan","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"e_1_2_2_3_1","volume-title":"SAS (Lecture Notes in Computer Science)","author":"Boyland John Tang"},{"key":"e_1_2_2_4_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","edition":"3"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1287\/opre.6.6.791"},{"key":"e_1_2_2_6_1","volume-title":"TACAS (Lecture Notes in Computer Science)","author":"de Moura Leonardo Mendon\u00e7a"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1102"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01840439"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","volume-title":"Modular Reasoning About Heap Paths via Effectively Propositional Formulas","author":"Itzhaky Shachar","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Shachar Itzhaky Anindya Banerjee Neil Immerman Aleksandar Nanevski and Mooly Sagiv. 2013. Effectively-Propositional Reasoning about Reachability in Linked Data Structures. In CAV Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg 756\u2013772.  Shachar Itzhaky Anindya Banerjee Neil Immerman Aleksandar Nanevski and Mooly Sagiv. 2013. Effectively-Propositional Reasoning about Reachability in Linked Data Structures. In CAV Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg 756\u2013772.","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"e_1_2_2_14_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. (2008). https:\/\/www.microsoft.com\/en- us\/research\/publication\/this- is- boogie- 2-2\/  K. Rustan M. Leino. 2008. This is Boogie 2. (2008). https:\/\/www.microsoft.com\/en- us\/research\/publication\/this- is- boogie- 2-2\/"},{"key":"e_1_2_2_15_1","volume-title":"Leino and Rosemary Monahan","author":"K. Rustan","year":"2009"},{"key":"e_1_2_2_16_1","volume-title":"Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5, 2","author":"Lev-Ami Tal","year":"2009"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1965.tb04146.x"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670416"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","volume-title":"The Binomial Heap Verification Challenge in Viper","author":"M\u00fcller Peter","DOI":"10.1007\/978-3-319-98047-8_13"},{"key":"e_1_2_2_20_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016"},{"key":"e_1_2_2_21_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016"},{"key":"e_1_2_2_22_1","volume-title":"Bierman","author":"Parkinson Matthew J.","year":"2005"},{"key":"e_1_2_2_23_1","volume-title":"Summers","author":"Parkinson Matthew J.","year":"2011"},{"key":"e_1_2_2_24_1","volume-title":"TACAS (Lecture Notes in Computer Science), Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.)","author":"Piskac Ruzica"},{"key":"e_1_2_2_25_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE Symposium on Logic in Computer Science (LICS \u201902)","author":"Reynolds John C.","year":"2002"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3367478"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the SPACE Workshop.","author":"Yang Hongseok","year":"2001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360547","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360547","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360547"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":29,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360547"],"URL":"https:\/\/doi.org\/10.1145\/3360547","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}