{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T17:05:52Z","timestamp":1751648752108,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NWO","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Concurrent separation logic has been responsible for major advances in the formal verification of fine-grained concurrent algorithms and data structures such as locks, barriers, queues, and reference counters. The key ingredient of the verification of a fine-grained program is an invariant, which relates the physical data representation (on the heap) to a logical representation (in mathematics) and to the state of the threads (using a form of ghost state). An invariant is typically represented as a disjunction of logical states, but this disjunctive nature makes invariants a difficult target for automated verification. Current approaches roughly suffer from two problems. They use backtracking to introduce disjunctions in an uninformed manner, which can lead to unprovable goals if an appropriate case analysis has not been made before choosing the disjunct. Moreover, they eliminate disjunctions too eagerly, which can cause poor efficiency.<\/jats:p>\n          <jats:p>\n            While disjunctions are no problem for automated provers based on classical (i.e., non-separating) logic, the challenges with disjunctions are prominent in the study of proof automation for intuitionistic logic. We take inspiration from that area\u2014specifically, based on ideas from\n            <jats:italic>connection calculus<\/jats:italic>\n            , we design a simple multi-succedent calculus for separation logic with disjunctions featuring a novel concept of a\n            <jats:italic>connection<\/jats:italic>\n            . While our calculus is not complete, it has the advantage that it can be extended with features of the state-of-the-art concurrent separation logic Iris (such as modalities, higher-order quantification, ghost state, and invariants), and can be implemented effectively in the Coq proof assistant with little need for backtracking. We evaluate the practicality on 24 challenging benchmarks, 14 of which we can verify fully automatically.\n          <\/jats:p>","DOI":"10.1145\/3591275","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1340-1364","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9926-9736","authenticated-orcid":false,"given":"Ike","family":"Mulder","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8083-4280","authenticated-orcid":false,"given":"\u0141ukasz","family":"Czajka","sequence":"additional","affiliation":[{"name":"TU Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_10"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/362759.362813"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/mmono\/067"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_8"},{"key":"e_1_2_1_16_1","volume-title":"ARQNL (IJCAR","volume":"63","author":"Galmiche Didier","year":"2018","unstructured":"Didier Galmiche and Daniel M\u00e9ry . 2018 . Labelled Connection-Based Proof Search for Multiplicative Intuitionistic Linear Logic . In ARQNL (IJCAR , Vol. 2095). 49\u2013 63 . http:\/\/ceur-ws.org\/Vol-2095\/paper3.pdf Didier Galmiche and Daniel M\u00e9ry. 2018. Labelled Connection-Based Proof Search for Multiplicative Intuitionistic Linear Logic. In ARQNL (IJCAR, Vol. 2095). 49\u201363. http:\/\/ceur-ws.org\/Vol-2095\/paper3.pdf"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_13"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63104-6_21"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151628"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_3"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535871"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPPS.1994.288305"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7799173"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586043"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39322-9_19"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_23"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59338-1_32"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications (Applied Logic Series","author":"Pym David J.","key":"e_1_2_1_47_1","unstructured":"David J. Pym . 2002. The Semantics and Proof Theory of the Logic of Bunched Implications (Applied Logic Series , Vol. 26). Kluwer. isbn:978-1-4020-0745- 3 David J. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications (Applied Logic Series, Vol. 26). Kluwer. isbn:978-1-4020-0745-3"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_50_1","unstructured":"Rust Language. 2021. Arc in Std::Sync - Rust. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Arc.html \t\t\t\t  Rust Language. 2021. Arc in Std::Sync - Rust. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Arc.html"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629678"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_55_1","volume-title":"Systems Programming: Coping with Parallelism. International Business Machines Incorporated","author":"Treiber Richard Kent","year":"1986","unstructured":"Richard Kent Treiber . 1986 . Systems Programming: Coping with Parallelism. International Business Machines Incorporated , Thomas J. Watson Research Center . Richard Kent Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center."},{"volume-title":"Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation","author":"Vafeiadis Viktor","key":"e_1_2_1_56_1","unstructured":"Viktor Vafeiadis . 2008. Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation . University of Cambridge . http:\/\/flint.cs.yale.edu\/cs428\/doc\/viktor-phd-thesis.pdf Viktor Vafeiadis. 2008. Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation. University of Cambridge. http:\/\/flint.cs.yale.edu\/cs428\/doc\/viktor-phd-thesis.pdf"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50024-2"},{"volume-title":"Automated Proof Search in Non-Classical Logics - Efficient Matrix Proof Methods for Modal and Intuitionistic Logics","author":"Wallen Lincoln A.","key":"e_1_2_1_58_1","unstructured":"Lincoln A. Wallen . 1990. Automated Proof Search in Non-Classical Logics - Efficient Matrix Proof Methods for Modal and Intuitionistic Logics . MIT Press . isbn:978-0-262-23144-2 Lincoln A. Wallen. 1990. Automated Proof Search in Non-Classical Logics - Efficient Matrix Proof Methods for Modal and Intuitionistic Logics. MIT Press. isbn:978-0-262-23144-2"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_27"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591275","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":60,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591275"],"URL":"https:\/\/doi.org\/10.1145\/3591275","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}