{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T09:02:13Z","timestamp":1788080533599,"version":"build-2784847793"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Over the past two decades, there has been a great deal of progress on verification of full functional correctness of programs using separation logic, sometimes even producing \u201cfoundational\u201d proofs in proof assistants like Coq. Unfortunately, even though existing approaches to this problem provide significant support for automated verification, they still incur a significant\n            <jats:italic toggle=\"yes\">specification overhead<\/jats:italic>\n            : the user must supply the specification against which the program is verified, and the specification may be long, complex, or tedious to formulate.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we introduce Quiver, the first technique for\n            <jats:italic toggle=\"yes\">inferring<\/jats:italic>\n            functional correctness specifications in separation logic while simultaneously verifying foundationally that they are correct. To guide Quiver towards the final specification, we take hints from the user in the form of\n            <jats:italic toggle=\"yes\">a specification sketch<\/jats:italic>\n            , and then complete the sketch using inference. To do so, Quiver introduces a new\n            <jats:italic toggle=\"yes\">abductive deductive verification<\/jats:italic>\n            technique, which integrates ideas from abductive inference (for specification inference) together with deductive separation logic automation (for foundational verification). The result is that users have to provide some guidance, but significantly less than with traditional deductive verification techniques based on separation logic. We have evaluated Quiver on a range of case studies, including code from popular open-source libraries.\n          <\/jats:p>","DOI":"10.1145\/3656413","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"889-913","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5424-9002","authenticated-orcid":false,"given":"Simon","family":"Spies","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2917-375X","authenticated-orcid":false,"given":"Lennard","family":"G\u00e4her","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi Isil Dillig and Arie Gurfinkel. 2016. Maximal specification synthesis. In POPL. ACM 789\u2013801. https:\/\/doi.org\/10.1145\/2837614.2837628 10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_29"},{"key":"e_1_3_1_5_2","unstructured":"Cristiano Calcagno Dino Distefano Peter O\u2019Hearn and Hongseok Yang. 2019. Go Huge or Go Home: POPL\u201919 Most Influential Paper Retrospective. https:\/\/blog.sigplan.org\/2020\/03\/03\/go-huge-or-go-home-popl19-most-influential-paper-retrospective\/"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter W. O\u2019Hearn and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In POPL. ACM 289\u2013300. https:\/\/doi.org\/10.1145\/1480881.1480917 10.1145\/1480881.1480917","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_10_2","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. USENIX Association 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_1_14_2","unstructured":"Coq. 2023. The Coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2019.00031"},{"key":"e_1_3_1_16_2","unstructured":"Cyrus IMAPD. 2023. Cyrus IMAPD Memory Wrapper Operations. https:\/\/github.com\/cyrusimap\/cyrus-imapd\/blob\/0552750789f23d205b50f582f73358d73cc15706\/lib\/xmalloc.c."},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-b-000588977"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_7"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_14"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_1_23_2","unstructured":"Git. 2023. Git Memory Wrapper Operations. https:\/\/github.com\/git\/git\/blob\/2e8e77cbac8ac17f94eee2087187fa1718e38b14\/wrapper.c."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41202-8_26"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.19"},{"key":"e_1_3_1_27_2","unstructured":"Infer. 2023. Infer. https:\/\/fbinfer.com."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Nico Lehmann Adam Geller Gilles Barthe Niki Vazou and Ranjit Jhala. 2023. Flux: Liquid Types for Rust. (2023). https:\/\/doi.org\/10.1145\/3591283 10.1145\/3591283","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498681"},{"issue":"1","key":"e_1_3_1_36_2","first-page":"5","article-title":"Inferring invariants in separation logic for imperative list-processing programs","volume":"1","author":"Magill Stephen","year":"2006","unstructured":"Stephen Magill, Aleksandar Nanevski, Edmund Clarke, and Peter Lee. 2006. Inferring invariants in separation logic for imperative list-processing programs. SPACE 1, 1 (2006), 5\u20137.","journal-title":"SPACE"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_1_38_2","unstructured":"memcached. 2023. memcached. https:\/\/www.memcached.org\/."},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45943-1_4"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_43_2","unstructured":"OpenSSL. 2023. OpenSSL. https:\/\/www.openssl.org."},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_28"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_1_49_2","unstructured":"Redis. 2023. Redis Memory Wrapper Operations. https:\/\/github.com\/redis\/redis\/blob\/3fac869f02657d94dc89fab23acb8ef188889c96\/src\/zmalloc.c."},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_25"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Michael Sammler and Derek Dreyer. 2024. Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq (Coq development and Appendix). https:\/\/doi.org\/10.5281\/zenodo.10940320 10.5281\/zenodo.10940320 Project webpage with appendix: https:\/\/plv.mpi-sws.org\/quiver\/.","DOI":"10.5281\/zenodo.10940320"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_8"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_21"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656413","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656413","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:46Z","timestamp":1751661766000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656413"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":59,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656413"],"URL":"https:\/\/doi.org\/10.1145\/3656413","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}