{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T14:59:46Z","timestamp":1780930786544,"version":"3.54.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>\n            Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, op-based CRDTs require that operations be propagated between replicas in causal order. This paper presents a framework for verifying safety properties of CRDT implementations using separation logic. The framework consists of two libraries. One implements a Reliable Causal Broadcast (RCB) protocol so that replicas can exchange messages in causal order. A second \u201cOpLib\u201d library then uses RCB to simplify the creation and correctness proofs of op-based CRDTs. OpLib allows clients to implement new CRDTs as purely-functional data structures, without having to reason about network operations, concurrency control and mutable state, and without having to each time re-implement causal broadcast. Using OpLib, we have implemented 12 example CRDTs from the literature, including multiple versions of replicated registers and sets, two CRDT combinators for products and maps, and two example use cases of the map combinator. Our proofs are conducted in the Aneris distributed separation logic and are formalized in Coq. Our technique is the first work on verification of op-based CRDTs that satisfies both of the following properties: it is\n            <jats:italic>modular<\/jats:italic>\n            and targets executable\n            <jats:italic>implementations<\/jats:italic>\n            , as opposed to high-level protocols.\n          <\/jats:p>","DOI":"10.1145\/3563351","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1788-1816","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Modular verification of op-based CRDTs in separation logic"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2741-8119","authenticated-orcid":false,"given":"Abel","family":"Nieto","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8262-6397","authenticated-orcid":false,"given":"L\u00e9on","family":"Gondelman","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4047-7770","authenticated-orcid":false,"given":"Alban","family":"Reynaud","sequence":"additional","affiliation":[{"name":"ENS Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2596631.2596632"},{"key":"e_1_2_1_4_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 \t\t\t\t  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_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/128738.128742"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_1_7_1","volume-title":"Introduction to Reliable and Secure Distributed Programming","author":"Cachin Christian","unstructured":"Christian Cachin , Rachid Guerraoui , and Lu\u00eds Rodrigues . 2011. Introduction to Reliable and Secure Distributed Programming . Springer Science & Business Media . Christian Cachin, Rachid Guerraoui, and Lu\u00eds Rodrigues. 2011. Introduction to Reliable and Secure Distributed Programming. Springer Science & Business Media."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365815.1365816"},{"key":"e_1_2_1_10_1","unstructured":"Kristina Chodorow and Michael Dirolf. 2010. MongoDB - The Definitive Guide: Powerful and Scalable Data Storage. O\u2019Reilly. \t\t\t\t  Kristina Chodorow and Michael Dirolf. 2010. MongoDB - The Definitive Guide: Powerful and Scalable Data Storage. O\u2019Reilly."},{"key":"e_1_2_1_11_1","unstructured":"Colin J Fidge. 1987. Timestamps in Message-Passing Systems That Preserve the Partial Ordering. \t\t\t\t  Colin J Fidge. 1987. Timestamps in Message-Passing Systems That Preserve the Partial Ordering."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3301419.3323971"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454067"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_24_1","unstructured":"Friedemann Mattern. 1988. Virtual Time and Global States of Distributed Systems. Univ. Department of Computer Science. \t\t\t\t  Friedemann Mattern. 1988. Virtual Time and Global States of Distributed Systems. Univ. Department of Computer Science."},{"key":"e_1_2_1_25_1","volume-title":"CAV (2) (Lecture Notes in Computer Science","author":"Nagar Kartik","unstructured":"Kartik Nagar and Suresh Jagannathan . 2019. Automated Parameterized Verification of CRDTs . In CAV (2) (Lecture Notes in Computer Science , Vol. 11562). Springer, 459\u2013 477 . Kartik Nagar and Suresh Jagannathan. 2019. Automated Parameterized Verification of CRDTs. In CAV (2) (Lecture Notes in Computer Science, Vol. 11562). Springer, 459\u2013477."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_20"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7055010"},{"key":"#cr-split#-e_1_2_1_28_1.1","unstructured":"Patrick Redmond Gan Shen Niki Vazou and Lindsey Kuper. 2022. Verified Causal Broadcast with Liquid Haskell. arXiv preprint arXiv:2206.14767 https:\/\/doi.org\/10.48550\/arXiv.2206.14767 10.48550\/arXiv.2206.14767"},{"key":"#cr-split#-e_1_2_1_28_1.2","unstructured":"Patrick Redmond Gan Shen Niki Vazou and Lindsey Kuper. 2022. Verified Causal Broadcast with Liquid Haskell. arXiv preprint arXiv:2206.14767 https:\/\/doi.org\/10.48550\/arXiv.2206.14767"},{"key":"e_1_2_1_29_1","volume-title":"Intensional Specifications of Security Protocols","author":"Roscoe A. W.","unstructured":"A. W. Roscoe . 1996. Intensional Specifications of Security Protocols . In CSFW. IEEE Computer Society , 28\u201338. A. W. Roscoe. 1996. Intensional Specifications of Security Protocols. In CSFW. IEEE Computer Society, 28\u201338."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Marc Shapiro Nuno Pregui\u00e7a Carlos Baquero and Marek Zawirski. 2011. A comprehensive study of Convergent and Commutative Replicated Data Types. INRIA. http:\/\/hal.inria.fr\/inria-00555588\/ \t\t\t\t  Marc Shapiro Nuno Pregui\u00e7a Carlos Baquero and Marek Zawirski. 2011. A comprehensive study of Convergent and Commutative Replicated Data Types. INRIA. http:\/\/hal.inria.fr\/inria-00555588\/","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213836.2213945"},{"key":"e_1_2_1_33_1","volume-title":"Tanenbaum and Maarten van Steen","author":"Andrew","year":"2007","unstructured":"Andrew S. Tanenbaum and Maarten van Steen . 2007 . Distributed systems - principles and paradigms, 2 nd Edition. Pearson Education . isbn:978-0-13-239227-3 Andrew S. Tanenbaum and Maarten van Steen. 2007. Distributed systems - principles and paradigms, 2nd Edition. Pearson Education. isbn:978-0-13-239227-3","edition":"2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439931"},{"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. arXiv preprint arXiv:2109.07863, https:\/\/doi.org\/10.48550\/arXiv.2109.07863 10.48550\/arXiv.2109.07863 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. arXiv preprint arXiv:2109.07863, https:\/\/doi.org\/10.48550\/arXiv.2109.07863"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3299869.3314049"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563351","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:33Z","timestamp":1750186953000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":39,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563351"],"URL":"https:\/\/doi.org\/10.1145\/3563351","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}