{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T23:05:38Z","timestamp":1778108738190,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:00:00Z","timestamp":1698019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-2123864"],"award-info":[{"award-number":["CCF-2123864"]}]},{"name":"NSF","award":["CCF-2318722"],"award-info":[{"award-number":["CCF-2318722"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,23]]},"DOI":"10.1145\/3600006.3613172","type":"proceedings-article","created":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T14:44:17Z","timestamp":1696344257000},"page":"113-129","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Grove: a Separation-Logic Library for Verifying Distributed Systems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5446-3284","authenticated-orcid":false,"given":"Upamanyu","family":"Sharma","sequence":"first","affiliation":[{"name":"CSAIL, MIT, Cambridge, MA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York City, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7098-586X","authenticated-orcid":false,"given":"Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"CSAIL, MIT, Cambridge, MA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0238-2703","authenticated-orcid":false,"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"CSAIL, MIT, Cambridge, MA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Ardekani Masoud Saeida","year":"2014","unstructured":"Masoud Saeida Ardekani and Douglas B. Terry . A self-configurable geo-replicated cloud storage system . In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , Broomfield, CO , October 2014 . Masoud Saeida Ardekani and Douglas B. Terry. A self-configurable geo-replicated cloud storage system. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Broomfield, CO, October 2014."},{"key":"e_1_3_2_1_2_1","first-page":"223","volume-title":"Proceedings of the 5th Conference on Innovative Data Systems Research (CIDR)","author":"Baker Jason","year":"2011","unstructured":"Jason Baker , Chris Bond , James C. Corbett , JJ Furman , Andrey Khorlin , James Larson , Jean-Michel Leon , Yawei Li , Alexander Lloyd , and Vadim Yushprakh . Megastore : Providing scalable, highly available storage for interactive services . In Proceedings of the 5th Conference on Innovative Data Systems Research (CIDR) , pages 223 -- 234 , Asilomar, CA , January 2011 . Jason Baker, Chris Bond, James C. Corbett, JJ Furman, Andrey Khorlin, James Larson, Jean-Michel Leon, Yawei Li, Alexander Lloyd, and Vadim Yushprakh. Megastore: Providing scalable, highly available storage for interactive services. In Proceedings of the 5th Conference on Innovative Data Systems Research (CIDR), pages 223--234, Asilomar, CA, January 2011."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Burrows Mike","year":"2006","unstructured":"Mike Burrows . The Chubby lock service for loosely-coupled distributed systems . In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , Seattle, WA , November 2006 . Mike Burrows. The Chubby lock service for loosely-coupled distributed systems. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Seattle, WA, November 2006."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2767386.2767415"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 423--439, Virtual conference","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed , Joseph Tassarotti , Mark Theng , Ralf Jung , M. Frans Kaashoek , and Nickolai Zeldovich . GoJournal : a verified, concurrent, crash-safe journaling system . In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 423--439, Virtual conference , July 2021 . Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. GoJournal: a verified, concurrent, crash-safe journaling system. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 423--439, Virtual conference, July 2021."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Chang Fay","year":"2006","unstructured":"Fay Chang , Jeffrey Dean , Sanjay Ghemawat , Wilson C. Hsieh , Deborah A. Wallach , Mike Burrows , Tushar Chandra , Andrew Fikes , and Robert E. Gruber . Bigtable: A distributed storage system for structured data . In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , Seattle, WA , November 2006 . Fay Chang, Jeffrey Dean, Sanjay Ghemawat, Wilson C. Hsieh, Deborah A. Wallach, Mike Burrows, Tushar Chandra, Andrew Fikes, and Robert E. Gruber. Bigtable: A distributed storage system for structured data. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Seattle, WA, November 2006."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Corbett James C.","year":"2012","unstructured":"James C. Corbett , Jeffrey Dean , Michael Epstein , Andrew Fikes , Christopher Frost , JJ Furman , Sanjay Ghemawat , Andrey Gubarev , Christopher Heiser , Peter Hochschild , Wilson Hsieh , Sebastian Kanthak , Eugene Kogan , Hongyi Li , Alexander Lloyd , Sergey Melnik , David Mwaura , David Nagle , Sean Quinlan , Rajesh Rao , Lindsay Rolig , Dale Woodford , Yasushi Saito , Christopher Taylor , Michal Szymaniak , and Ruth Wang . Spanner : Google's globally-distributed database . In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , Hollywood, CA , October 2012 . James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, JJ Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Dale Woodford, Yasushi Saito, Christopher Taylor, Michal Szymaniak, and Ruth Wang. Spanner: Google's globally-distributed database. In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Hollywood, CA, October 2012."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815425"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 2022 USENIX Annual Technical Conference","author":"Elhemali Mostafa","year":"2022","unstructured":"Mostafa Elhemali , Niall Gallagher , Nicholas Gordon , Joseph Idziorek , Richard Krog , Colin Lazier , Erben Mo , Akhilesh Mritunjai , Somu Perianayagam , Tim Rath , Swami Sivasubramanian , James Christopher Sorenson III, Sroaj Sosothikul , Doug Terry , and Akshat Vig . Amazon DynamoDB : A scalable, predictably performant, and fully managed NoSQL database service . In Proceedings of the 2022 USENIX Annual Technical Conference , Carlsbad, CA , July 2022 . Mostafa Elhemali, Niall Gallagher, Nicholas Gordon, Joseph Idziorek, Richard Krog, Colin Lazier, Erben Mo, Akhilesh Mritunjai, Somu Perianayagam, Tim Rath, Swami Sivasubramanian, James Christopher Sorenson III, Sroaj Sosothikul, Doug Terry, and Akshat Vig. Amazon DynamoDB: A scalable, predictably performant, and fully managed NoSQL database service. In Proceedings of the 2022 USENIX Annual Technical Conference, Carlsbad, CA, July 2022."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945450"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_3_2_1_16_1","first-page":"202","volume-title":"Proceedings of the 12th ACM Symposium on Operating Systems Principles (SOSP)","author":"Cary","year":"1989","unstructured":"Cary G. Gray and David R. Cheriton. Leases: An efficient fault-tolerant mechanism for distributed file cache consistency . In Proceedings of the 12th ACM Symposium on Operating Systems Principles (SOSP) , pages 202 -- 210 , Litchfield Park, AZ , December 1989 . Cary G. Gray and David R. Cheriton. Leases: An efficient fault-tolerant mechanism for distributed file cache consistency. In Proceedings of the 12th ACM Symposium on Operating Systems Principles (SOSP), pages 202--210, Litchfield Park, AZ, December 1989."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hance Travis","year":"2023","unstructured":"Travis Hance , Yi Zhou , Andrea Lattuada , Reto Achermann , Alex Conway , Ryan Stutsman , Gerd Zellweger , Chris Hawblitzel , Jon Howell , and Bryan Parno . Sharding the state machine: Automated modular reasoning for complex concurrent systems . In Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , Boston, MA , July 2023 . Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Boston, MA, July 2023."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-912-1_8"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL)","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung , David Swasey , Filip Sieczkowski , Kasper Svendsen , Aaron Turon , Lars Birkedal , and Derek Dreyer . Iris : Monoids and invariants as an orthogonal basis for concurrent reasoning . In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL) , Mumbai, India , January 2015 . Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL), Mumbai, India, January 2015."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_24_1","volume-title":"https:\/\/cwiki.apache.org\/confluence\/display\/kafka\/kafka+replication","author":"Kafka Apache","year":"2013","unstructured":"Apache Kafka . https:\/\/cwiki.apache.org\/confluence\/display\/kafka\/kafka+replication , 2013 . Accessed : 2023-04-10. Apache Kafka. https:\/\/cwiki.apache.org\/confluence\/display\/kafka\/kafka+replication, 2013. Accessed: 2023-04-10."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_3_2_1_26_1","first-page":"327","volume-title":"Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation","author":"Konnov Igor","year":"2018","unstructured":"Igor Konnov and Josef Widder . ByMC : Byzantine model checker . In Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation , pages 327 -- 342 , Limassol, Cyprus , November 2018 . Igor Konnov and Josef Widder. ByMC: Byzantine model checker. In Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, pages 327--342, Limassol, Cyprus, November 2018."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_30_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley , 2002 . ISBN 0-3211-4306-X. Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. ISBN 0-3211-4306-X."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_1_32_1","first-page":"105","volume-title":"Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"MacCormick John","year":"2004","unstructured":"John MacCormick , Nick Murphy , Marc Najork , Chandramohan A. Thekkath , and Lidong Zhou . Boxwood : Abstractions as the foundation for storage infrastructure . In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 105 -- 120 , San Francisco, CA , December 2004 . John MacCormick, Nick Murphy, Marc Najork, Chandramohan A. Thekkath, and Lidong Zhou. Boxwood: Abstractions as the foundation for storage infrastructure. In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 105--120, San Francisco, CA, December 2004."},{"key":"e_1_3_2_1_33_1","first-page":"190","volume-title":"Proceedings of the 32nd International Conference on Computer Aided Verification (CAV)","author":"Kenneth","year":"2020","unstructured":"Kenneth L. McMillan and Oded Padon. Ivy: A multimodal verification tool for distributed algorithms . In Proceedings of the 32nd International Conference on Computer Aided Verification (CAV) , pages 190 -- 202 , Los Angeles, CA , July 2020 . Kenneth L. McMillan and Oded Padon. Ivy: A multimodal verification tool for distributed algorithms. In Proceedings of the 32nd International Conference on Computer Aided Verification (CAV), pages 190--202, Los Angeles, CA, July 2020."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_37_1","volume-title":"Modular verification of distributed systems with Grove. Master's thesis","author":"Sharma Upamanyu","year":"2022","unstructured":"Upamanyu Sharma . Modular verification of distributed systems with Grove. Master's thesis , Massachusetts Institute of Technology , Department of Electrical Engineering and Computer Science, September 2022 . Upamanyu Sharma. Modular verification of distributed systems with Grove. Master's thesis, Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, September 2022."},{"key":"e_1_3_2_1_38_1","volume-title":"September","author":"Sharma Upamanyu","year":"2023","unstructured":"Upamanyu Sharma , Ralf Jung , Joseph Tassarotti , M. Frans Kaashoek , and Nickolai Zeldovich . Grove: a separation-logic library for verifying distributed systems (extended version). arXiv:2309.03046 [cs.LO] , September 2023 . Available at https:\/\/arxiv.org\/abs\/2309.03046. Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Grove: a separation-logic library for verifying distributed systems (extended version). arXiv:2309.03046 [cs.LO], September 2023. Available at https:\/\/arxiv.org\/abs\/2309.03046."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8161141"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"van Renesse Robbert","year":"2004","unstructured":"Robbert van Renesse and Fred B. Schneider . Chain replication for supporting high throughput and availability . In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , San Francisco, CA , December 2004 . Robbert van Renesse and Fred B. Schneider. Chain replication for supporting high throughput and availability. In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI), San Francisco, CA, December 2004."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3448016.3457559"}],"event":{"name":"SOSP '23: 29th Symposium on Operating Systems Principles","location":"Koblenz Germany","acronym":"SOSP '23","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the 29th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3600006.3613172","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3600006.3613172","content-type":"text\/html","content-version":"vor","intended-application":"syndication"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:49Z","timestamp":1750178209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3600006.3613172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":42,"alternative-id":["10.1145\/3600006.3613172","10.1145\/3600006"],"URL":"https:\/\/doi.org\/10.1145\/3600006.3613172","relation":{},"subject":[],"published":{"date-parts":[[2023,10,23]]},"assertion":[{"value":"2023-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}