{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:48:12Z","timestamp":1777348092262,"version":"3.51.4"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"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,4,6]]},"abstract":"<jats:p>\n            Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained (\n            <jats:italic>i.e.<\/jats:italic>\n            , lock-free) concurrent programs. For such programs, the golden standard of correctness is\n            <jats:italic>linearizability<\/jats:italic>\n            , which expresses that concurrent executions always behave as some valid sequence of sequential executions. Compositional approaches to linearizability (such as contextual refinement and logical atomicity) make it possible to prove linearizability of whole programs or compound data structures (\n            <jats:italic>e.g.<\/jats:italic>\n            , a ticket lock) using proofs of linearizability of their individual components (\n            <jats:italic>e.g.<\/jats:italic>\n            , a counter). While powerful, these approaches are also laborious\u2014state-of-the-art tools such as Iris, FCSL, and Voila all require a form of interactive proof.\n          <\/jats:p>\n          <jats:p>This paper develops proof automation for contextual refinement and logical atomicity in Iris. The key ingredient of our proof automation is a collection of proof rules whose application is directed by both the program and the logical state. This gives rise to effective proof search strategies that can prove linearizability of simple examples fully automatically. For more complex examples, we ensure the proof automation cooperates well with interactive proof tactics by minimizing the use of backtracking.<\/jats:p>\n          <jats:p>We implement our proof automation in Coq by extending and generalizing Diaframe, a proof automation extension for Iris. While the old version (Diaframe 1.0) was limited to ordinary Hoare triples, the new version (Diaframe 2.0) is extensible in its support for program verification styles: our proof search strategies for contextual refinement and logical atomicity are implemented as modules for Diaframe 2.0. We evaluate our proof automation on a set of existing benchmarks and novel proofs, showing that it provides significant reduction of proof work for both approaches to linearizability.<\/jats:p>","DOI":"10.1145\/3586043","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"462-491","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Proof Automation for Linearizability in 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-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,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542667"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503681"},{"key":"e_1_2_1_9_1","unstructured":"Tej Chajed Joseph Tassarotti Mark Theng Ralf Jung M. Frans Kaashoek and Nickolai Zeldovich. 2021. GoJournal: A Verified Concurrent Crash-Safe Journaling System. In OSDI. 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed \t\t\t\t  Tej Chajed Joseph Tassarotti Mark Theng Ralf Jung M. Frans Kaashoek and Nickolai Zeldovich. 2021. GoJournal: A Verified Concurrent Crash-Safe Journaling System. In OSDI. 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.25560\/47923"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_34"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36108-1_18"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_1_33_1","unstructured":"Ralf Jung. 2019. Logical Atomicity in Iris: The Good the Bad and the Ugly. https:\/\/people.mpi-sws.org\/~jung\/iris\/logatom-talk-2019.pdf Slides of talk given at Iris Workshop 2019 \t\t\t\t  Ralf Jung. 2019. Logical Atomicity in Iris: The Good the Bad and the Ugly. https:\/\/people.mpi-sws.org\/~jung\/iris\/logatom-talk-2019.pdf Slides of talk given at Iris Workshop 2019"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_23"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01806-0"},{"key":"e_1_2_1_46_1","unstructured":"K Rustan M Leino and Micha\u0142 Moskal. 2010. Usable Auto-Active Verification. https:\/\/fm.csl.sri.com\/UV10\/submissions\/uv2010_submission_20.pdf \t\t\t\t  K Rustan M Leino and Micha\u0142 Moskal. 2010. Usable Auto-Active Verification. https:\/\/fm.csl.sri.com\/UV10\/submissions\/uv2010_submission_20.pdf"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"#cr-split#-e_1_2_1_48_1.1","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. https:\/\/doi.org\/10.48550\/arXiv.2207.06574 arxiv:arXiv:2207.06574. 10.48550\/arXiv.2207.06574"},{"key":"#cr-split#-e_1_2_1_48_1.2","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. https:\/\/doi.org\/10.48550\/arXiv.2207.06574 arxiv:arXiv:2207.06574."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_50_1","volume-title":"Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. https:\/\/ikemulder.nl\/media\/papers\/diaframe-vee-draft.pdf Manuscript","author":"Mulder Ike","year":"2023","unstructured":"Ike Mulder , \u0141ukasz Czajka , and Robbert Krebbers . 2023 . Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. https:\/\/ikemulder.nl\/media\/papers\/diaframe-vee-draft.pdf Manuscript Ike Mulder, \u0141ukasz Czajka, and Robbert Krebbers. 2023. Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. https:\/\/ikemulder.nl\/media\/papers\/diaframe-vee-draft.pdf Manuscript"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7712620"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360587"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_2_1_58_1","volume-title":"Advanced Topics in Types and Programming Languages, Benjamin C","author":"Pitts Andrew M.","unstructured":"Andrew M. Pitts . 2005. Typed Operational Reasoning . In Advanced Topics in Types and Programming Languages, Benjamin C . Pierce (Ed.). MIT Press , 245\u2013289. Andrew M. Pitts. 2005. Typed Operational Reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, 245\u2013289."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_1_66_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."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503689"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_22"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586043","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586043","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:11Z","timestamp":1750178771000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586043"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":73,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586043"],"URL":"https:\/\/doi.org\/10.1145\/3586043","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}