{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:39Z","timestamp":1775873679182,"version":"3.50.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"VILLUM Foundation","award":["25804"],"award-info":[{"award-number":["25804"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top of UDP and features characteristic traits of existing protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission\/acknowledgement mechanisms. We verify the library in the Aneris distributed separation logic using a novel proof pattern---dubbed the session escrow pattern---based on the existing escrow proof pattern and the so-called dependent separation protocols, which hitherto have only been used in a non-distributed concurrent setting. We demonstrate how our specification of the reliable communication library simplifies formal reasoning about applications, such as a remote procedure call library, which we in turn use to verify a lazily replicated key-value store with leader-followers and clients thereof. Our development is highly modular---each component is verified relative to specifications of the components it uses (not the implementation). All our results are formalized in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3607859","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"847-877","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8262-6397","authenticated-orcid":false,"given":"L\u00e9on","family":"Gondelman","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7048-9425","authenticated-orcid":false,"given":"M\u00e1rio","family":"Pereira","sequence":"additional","affiliation":[{"name":"NOVA-LINCS, Portugal \/ NOVA School of Sciences and Tecnhology, Portugal"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0070-0"},{"key":"e_1_2_1_2_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Log. http:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290342"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_6_1","volume-title":"Eleventh CATS 2005, Computing: The Australasian Theory Symposium, Newcastle, NSW, Australia, January\/February","volume":"30","author":"Compton Michael","year":"2005","unstructured":"Michael Compton. 2005. Stenning\u2019s Protocol Implemented in UDP and Verified in Isabelle. In Theory of Computing 2005, Eleventh CATS 2005, Computing: The Australasian Theory Symposium, Newcastle, NSW, Australia, January\/February 2005, Mike D. Atkinson and Frank K. H. A. Dehne (Eds.) (CRPIT, Vol. 41). Australian Computer Society, 21\u201330. http:\/\/crpit.scem.westernsydney.edu.au\/abstracts\/CRPITV41Compton.html"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/174147.169676"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8121688"},{"key":"e_1_2_1_11_1","unstructured":"James N Gray. 1979. A discussion of distributed systems."},{"key":"e_1_2_1_12_1","volume-title":"Failure Recovery: When the Cure Is Worse Than the Disease. In 14th Workshop on Hot Topics in Operating Systems, HotOS XIV, Santa Ana Pueblo","author":"Guo Zhenyu","year":"2013","unstructured":"Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Madan Musuvathi, Zheng Zhang, and Lidong Zhou. 2013. Failure Recovery: When the Cure Is Worse Than the Disease. In 14th Workshop on Hot Topics in Operating Systems, HotOS XIV, Santa Ana Pueblo, New Mexico, USA, May 13-15, 2013. https:\/\/www.usenix.org\/conference\/hotos13\/session\/guo"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev.cs.02.060187.000345"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.03.028"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_23_1","volume-title":"Gay","author":"Kouzapas Dimitrios","year":"2019","unstructured":"Dimitrios Kouzapas, Ramunas Gutkovas, A. Laura Voinea, and Simon J. Gay. 2019. A Session Type System for Asynchronous Unreliable Broadcast Communication. CoRR, abs\/1902.01353 (2019), arXiv:1902.01353. arxiv:1902.01353"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3446804.3446854"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563351"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"M. A. S. Smith. 1996. Formal Verification of Communication Protocols. In FORTE.","DOI":"10.1007\/978-0-387-35079-0_8"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_2_1_35_1","volume-title":"L\u00e9o Stefanesco, L\u00e9on Gondelman, Abel Nieto, and Lars Birkedal.","author":"Timany Amin","year":"2021","unstructured":"Amin Timany, Simon Oddershede Gregersen, L\u00e9o Stefanesco, L\u00e9on Gondelman, Abel Nieto, and Lars Birkedal. 2021. Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. CoRR, abs\/2109.07863 (2021), arXiv:2109.07863. arxiv:2109.07863"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607859","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607859"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607859"],"URL":"https:\/\/doi.org\/10.1145\/3607859","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}