{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:25Z","timestamp":1763054605083,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T00:00:00Z","timestamp":1760313600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2019285,2442888"],"award-info":[{"award-number":["2019285,2442888"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100014188","name":"Ministry of Science and ICT, South Korea","doi-asserted-by":"publisher","award":["RS-2024-00459026,RS-2025-00556905"],"award-info":[{"award-number":["RS-2024-00459026,RS-2025-00556905"]}],"id":[{"id":"10.13039\/501100014188","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768331","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"42-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Model-Driven Verification of Weakly Consistent Distributed Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-1096-9893","authenticated-orcid":false,"given":"Bryant J.","family":"Curto","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7070-3578","authenticated-orcid":false,"given":"Jeonghyeon","family":"Kim","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7774-023X","authenticated-orcid":false,"given":"Alan","family":"Wang","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0280-4451","authenticated-orcid":false,"given":"Gijung","family":"Im","sequence":"additional","affiliation":[{"name":"Yonsei University, Seoul, Republic of Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7581-041X","authenticated-orcid":false,"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yonsei University, Seoul, Republic of Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2115-0871","authenticated-orcid":false,"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"FuriosaAI, Seoul, Republic of Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1595-4849","authenticated-orcid":false,"given":"Ji-Yong","family":"Shin","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2024. Azure Cosmos DB. https:\/\/azure.microsoft.com\/en-us\/products\/cosmos-db\/."},{"key":"e_1_3_2_1_2_1","unstructured":"2024. Iris Project. https:\/\/iris-project.org."},{"key":"e_1_3_2_1_3_1","unstructured":"2024. Sequential consistency without borders: how D1 implements global read replication. https:\/\/blog.cloudflare.com\/d1-read-replication-beta\/."},{"key":"e_1_3_2_1_4_1","unstructured":"2025. Goose: a subset of Go with a semantics in Coq. https:\/\/github.com\/goose-lang\/goose."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_6_1","volume-title":"Defining liveness. Information processing letters 21, 4","author":"Alpern Bowen","year":"1985","unstructured":"Bowen Alpern and Fred B Schneider. 1985. Defining liveness. Information processing letters 21, 4 (1985), 181--185."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2447976.2447992"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535877"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMPDP.2004.1271440"},{"volume-title":"Session Guarantees to Achieve PRAM Consistency of Replicated Shared Objects","author":"Brzezinski Jerzy","key":"e_1_3_2_1_10_1","unstructured":"Jerzy Brzezinski, Cezary Sobaniec, and Dariusz Wawrzyniak. 2004. Session Guarantees to Achieve PRAM Consistency of Replicated Shared Objects. In Parallel Processing and Applied Mathematics, Roman Wyrzykowski, Jack Dongarra, Marcin Paprzycki, and Jerzy Wa\u015bniewski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1--8."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/296806.296824"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.14778\/1454159.1454167"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1323293.1294281"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41841"},{"volume-title":"Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback","author":"Gelashvili Rati","key":"e_1_3_2_1_16_1","unstructured":"Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. 2022. Jolteon and Ditto: Network-Adaptive Efficient Consensus with Asynchronous Fallback. In Financial Cryptography and Data Security, Ittay Eyal and Juan Garay (Eds.). Springer International Publishing, Cham, 296--315."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1165389.945450"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133933"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409005"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proc. 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16). 653--669."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522722"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_29_1","unstructured":"Butler Lampson. 2021. Hints and Principles for Computer System Design. arXiv:2011.02455 [cs.DC]"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_3_2_1_32_1","volume-title":"USENIX Annual Technical Conference. 305--319","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John K Ousterhout. 2014. In Search of an Understandable Consensus Algorithm.. In USENIX Annual Technical Conference. 305--319."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656423"},{"volume-title":"Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago","author":"Shapiro Marc","key":"e_1_3_2_1_34_1","unstructured":"Marc Shapiro, Nuno Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011. Conflict-Free Replicated Data Types. In Stabilization, Safety, and Security of Distributed Systems, Xavier D\u00e9fago, Franck Petit, and Vincent Villain (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 386--400."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2987550.2987579"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357223.3362739"},{"key":"e_1_3_2_1_38_1","volume-title":"Tanenbaum and Maarten van Steen","author":"Andrew","year":"2006","unstructured":"Andrew S. Tanenbaum and Maarten van Steen. 2006. Distributed Systems: Principles and Paradigms (2Nd Edition). Prentice-Hall, Inc."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500500"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDIS.1994.331722"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522731"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/224057.224070"},{"key":"e_1_3_2_1_43_1","unstructured":"The Rocq development team. 2025. The Rocq prover. https:\/\/rocq-prover.org."},{"key":"e_1_3_2_1_44_1","first-page":"91","article-title":"Chain Replication for Supporting High Throughput and Availability","volume":"4","author":"Renesse Robbert Van","year":"2004","unstructured":"Robbert Van Renesse and Fred B Schneider. 2004. Chain Replication for Supporting High Throughput and Availability.. In OSDI, Vol. 4. 91--104.","journal-title":"OSDI"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2926965"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.2018.00044"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331591"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3764860.3768331","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768331","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:19:51Z","timestamp":1763054391000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":49,"alternative-id":["10.1145\/3764860.3768331","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768331","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}