{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:28:41Z","timestamp":1770272921021,"version":"3.49.0"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1846327,CCF-1908504"],"award-info":[{"award-number":["CCF-1846327,CCF-1908504"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007289","name":"Purdue Research Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100007289","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.<\/jats:p>","DOI":"10.1145\/3485534","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["QuickSilver: modeling and parameterized verification for distributed agreement-based systems"],"prefix":"10.1145","volume":"5","author":[{"given":"Nouraldin","family":"Jaber","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Christopher","family":"Wagner","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[{"name":"CISPA, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6827-345X","authenticated-orcid":false,"given":"Milind","family":"Kulkarni","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Hardware and Software: Verification and Testing","author":"Alur Rajeev","unstructured":"Rajeev Alur , Milo Martin , Mukund Raghothaman , Christos Stergiou , Stavros Tripakis , and Abhishek Udupa . 2014. Synthesizing Finite-State Protocols from Scenarios and Requirements . In Hardware and Software: Verification and Testing , Eran Yahav (Ed.). Springer International Publishing , Cham . 75\u201391. isbn:978-3-319-13338-6 Rajeev Alur, Milo Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa. 2014. Synthesizing Finite-State Protocols from Scenarios and Requirements. In Hardware and Software: Verification and Testing, Eran Yahav (Ed.). Springer International Publishing, Cham. 75\u201391. isbn:978-3-319-13338-6"},{"key":"e_1_2_2_2_1","volume-title":"Automatic Completion of Distributed Protocols with Symmetry","author":"Alur Rajeev","unstructured":"Rajeev Alur , Mukund Raghothaman , Christos Stergiou , Stavros Tripakis , and Abhishek Udupa . 2015. Automatic Completion of Distributed Protocols with Symmetry . In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing , Cham . 395\u2013412. isbn:978-3-319-21668-3 Rajeev Alur, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa. 2015. Automatic Completion of Distributed Protocols with Symmetry. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham. 395\u2013412. isbn:978-3-319-21668-3"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3061640.3061652"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-017-0302-6"},{"key":"e_1_2_2_5_1","unstructured":"Zachary Amsden Ramnik Arora Shehar Bano Mathieu Baudet Sam Blackshear Abhay Bothra George Cabrera andChristian Catalini Konstantinos Chalkias Evan Cheng Avery Ching Andrey Chursin George Danezis andGerardo Di Giacomo David L. Dill Hui Ding Nick Doudchenko Victor Gao Zhenhuan Gao Fran\u00e7ois Garillot Michael Gorven Philip Hayes J. Mark Hou Yuxuan Hu Kevin Hurley Kevin Lewi Chunqi Li Zekun Li Dahlia Malkhi andSonia Margulis Ben Maurer Payman Mohassel Ladi de Naurois Valeria Nikolaenko Todd Nowacki Oleksandr Orlov andDmitri Perelman Alistair Pott Brett Proctor Shaz Qadeer Rain Dario Russi Bryan Schwab Stephane Sezer Alberto Sonnino Herman Venter Lei Wei Nils Wernerfelt Brandon Williams Qinfan Wu Xifan Yan Tim Zakian and Runtian Zhou. 2020. The Libra Blockchain. https:\/\/developers.libra.org\/docs\/assets\/papers\/the-libra-blockchain\/2020-05-26.pdf  Zachary Amsden Ramnik Arora Shehar Bano Mathieu Baudet Sam Blackshear Abhay Bothra George Cabrera andChristian Catalini Konstantinos Chalkias Evan Cheng Avery Ching Andrey Chursin George Danezis andGerardo Di Giacomo David L. Dill Hui Ding Nick Doudchenko Victor Gao Zhenhuan Gao Fran\u00e7ois Garillot Michael Gorven Philip Hayes J. Mark Hou Yuxuan Hu Kevin Hurley Kevin Lewi Chunqi Li Zekun Li Dahlia Malkhi andSonia Margulis Ben Maurer Payman Mohassel Ladi de Naurois Valeria Nikolaenko Todd Nowacki Oleksandr Orlov andDmitri Perelman Alistair Pott Brett Proctor Shaz Qadeer Rain Dario Russi Bryan Schwab Stephane Sezer Alberto Sonnino Herman Venter Lei Wei Nils Wernerfelt Brandon Williams Qinfan Wu Xifan Yan Tim Zakian and Runtian Zhou. 2020. The Libra Blockchain. https:\/\/developers.libra.org\/docs\/assets\/papers\/the-libra-blockchain\/2020-05-26.pdf"},{"key":"e_1_2_2_6_1","volume-title":"Practical Aspects of Declarative Languages, Jos\u00e9 J\u00falio Alferes and Moa Johansson (Eds.)","author":"Arndal Andersen Kristoffer Just","unstructured":"Kristoffer Just Arndal Andersen and Ilya Sergey . 2019. Distributed Protocol Combinators . In Practical Aspects of Declarative Languages, Jos\u00e9 J\u00falio Alferes and Moa Johansson (Eds.) . Springer International Publishing , Cham . 169\u2013186. isbn:978-3-030-05998-9 Kristoffer Just Arndal Andersen and Ilya Sergey. 2019. Distributed Protocol Combinators. In Practical Aspects of Declarative Languages, Jos\u00e9 J\u00falio Alferes and Moa Johansson (Eds.). Springer International Publishing, Cham. 169\u2013186. isbn:978-3-030-05998-9"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICIMU.2011.6122724"},{"key":"e_1_2_2_9_1","unstructured":"Atomix. 2021. Atomix. https:\/\/atomix.io\/docs\/latest\/user-manual\/primitives\/AtomicValue\/  Atomix. 2021. Atomix. https:\/\/atomix.io\/docs\/latest\/user-manual\/primitives\/AtomicValue\/"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_23"},{"key":"e_1_2_2_11_1","volume-title":"Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems","author":"Bloem Roderick","unstructured":"Roderick Bloem , Nicolas Braud-Santoni , and Swen Jacobs . 2016. Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems . In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing , Cham . 157\u2013176. isbn:978-3-319-41528-4 Roderick Bloem, Nicolas Braud-Santoni, and Swen Jacobs. 2016. Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 157\u2013176. isbn:978-3-319-41528-4"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1298455.1298487"},{"key":"e_1_2_2_13_1","volume-title":"Stabilization, Safety, and Security of Distributed Systems, Toshimitsu Masuzawa and S\u00e9bastien Tixeuil (Eds.)","author":"Canepa Davide","unstructured":"Davide Canepa and Maria Gradinariu Potop-Butucaru . 2007. Stabilizing Flocking Via Leader Election in Robot Networks . In Stabilization, Safety, and Security of Distributed Systems, Toshimitsu Masuzawa and S\u00e9bastien Tixeuil (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg . 52\u201366. isbn:978-3-540-76627-8 Davide Canepa and Maria Gradinariu Potop-Butucaru. 2007. Stabilizing Flocking Via Leader Election in Robot Networks. In Stabilization, Safety, and Security of Distributed Systems, Toshimitsu Masuzawa and S\u00e9bastien Tixeuil (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 52\u201366. isbn:978-3-540-76627-8"},{"key":"e_1_2_2_14_1","volume-title":"Stoller","author":"Chand Saksham","year":"2016","unstructured":"Saksham Chand , Yanhong A. Liu , and Scott D . Stoller . 2016 . Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods, John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer International Publishing , Cham. 119\u2013136. isbn:978-3-319-48989-6 Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. 2016. Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods, John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer International Publishing, Cham. 119\u2013136. isbn:978-3-319-48989-6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-wss.2015.0030"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0084-6"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"e_1_2_2_19_1","volume-title":"Communication-closed Asynchronous Protocols. In International Conference on Computer Aided Verification.","author":"Damian Andrei","year":"2019","unstructured":"Andrei Damian , Cezara Dragoi , Alexandru Militaru , and Josef Widder . 2019 . Communication-closed Asynchronous Protocols. In International Conference on Computer Aided Verification. Andrei Damian, Cezara Dragoi, Alexandru Militaru, and Josef Widder. 2019. Communication-closed Asynchronous Protocols. In International Conference on Computer Aided Verification."},{"key":"e_1_2_2_20_1","volume-title":"Automatic Compositional Synthesis of Distributed Systems. In International Symposium on Formal Methods. 179\u2013193","author":"Damm Werner","year":"2014","unstructured":"Werner Damm and Bernd Finkbeiner . 2014 . Automatic Compositional Synthesis of Distributed Systems. In International Symposium on Formal Methods. 179\u2013193 . Werner Damm and Bernd Finkbeiner. 2014. Automatic Compositional Synthesis of Distributed Systems. In International Symposium on Formal Methods. 179\u2013193."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_13"},{"key":"e_1_2_2_22_1","first-page":"4965","volume-title":"Proceedings of the 8th International Conference on Cyber-Physical Systems (ICCPS \u201917)","author":"Desai Ankush","unstructured":"Ankush Desai , Indranil Saha , Jianqiao Yang , Shaz Qadeer , and Sanjit A. Seshia . 2017. DRONA: A Framework for Safe Distributed Mobile Robotics . In Proceedings of the 8th International Conference on Cyber-Physical Systems (ICCPS \u201917) . ACM, 239\u2013248. isbn:978-1-4503- 4965 - 4969 Ankush Desai, Indranil Saha, Jianqiao Yang, Shaz Qadeer, and Sanjit A. Seshia. 2017. DRONA: A Framework for Safe Distributed Mobile Robotics. In Proceedings of the 8th International Conference on Cyber-Physical Systems (ICCPS \u201917). ACM, 239\u2013248. isbn:978-1-4503-4965-9"},{"key":"e_1_2_2_23_1","unstructured":"Ryan Doenges James R Wilcox Doug Woos Zachary Tatlock and Karl Palmskog. 2017. Verification of Implementations of Distributed Systems Under Churn.  Ryan Doenges James R Wilcox Doug Woos Zachary Tatlock and Karl Palmskog. 2017. Verification of Implementations of Distributed Systems Under Churn."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837650"},{"key":"e_1_2_2_26_1","volume-title":"CHARME (Lecture Notes in Computer Science","volume":"262","author":"Allen Emerson E.","year":"2003","unstructured":"E. Allen Emerson and Vineet Kahlon . 2003 . Exact and Efficient Verification of Parameterized Cache CoherenceProtocols . In CHARME (Lecture Notes in Computer Science , Vol. 2860). Springer, 247\u2013 262 . E. Allen Emerson and Vineet Kahlon. 2003. Exact and Efficient Verification of Parameterized Cache CoherenceProtocols. In CHARME (Lecture Notes in Computer Science, Vol. 2860). Springer, 247\u2013262."},{"key":"e_1_2_2_27_1","volume-title":"Model Checking Guarded Protocols. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. IEEE Computer Society, 361\u2013370","author":"Allen Emerson E.","year":"2003","unstructured":"E. Allen Emerson and Vineet Kahlon . 2003 . Model Checking Guarded Protocols. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. IEEE Computer Society, 361\u2013370 . E. Allen Emerson and Vineet Kahlon. 2003. Model Checking Guarded Protocols. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings. IEEE Computer Society, 361\u2013370."},{"key":"e_1_2_2_28_1","volume-title":"Symmetry and Model Checking. Formal methods in system design, 9, 1-2","author":"Allen Emerson E.","year":"1996","unstructured":"E. Allen Emerson and A Prasad Sistla . 1996. Symmetry and Model Checking. Formal methods in system design, 9, 1-2 ( 1996 ), 105\u2013131. E. Allen Emerson and A Prasad Sistla. 1996. Symmetry and Model Checking. Formal methods in system design, 9, 1-2 (1996), 105\u2013131."},{"key":"e_1_2_2_29_1","volume-title":"On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods. 216\u2013230","author":"Allen Emerson E.","year":"2003","unstructured":"E. Allen Emerson and Thomas Wahl . 2003 . On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods. 216\u2013230 . E. Allen Emerson and Thomas Wahl. 2003. On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods. 216\u2013230."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782630"},{"key":"e_1_2_2_31_1","volume-title":"Inferring Inductive Invariants from Phase Structures","author":"Feldman Yotam M. Y.","unstructured":"Yotam M. Y. Feldman , James R. Wilcox , Sharon Shoham , and Mooly Sagiv . 2019. Inferring Inductive Invariants from Phase Structures . In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing , Cham . 405\u2013425. isbn:978-3-030-25543-5 Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv. 2019. Inferring Inductive Invariants from Phase Structures. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham. 405\u2013425. isbn:978-3-030-25543-5"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1675885"},{"key":"e_1_2_2_33_1","volume-title":"Deconstructed and Abstracted","author":"Garc\u00eda-P\u00e9rez \u00c1lvaro","unstructured":"\u00c1lvaro Garc\u00eda-P\u00e9rez , Alexey Gotsman , Yuri Meshman , and Ilya Sergey . 2018. Paxos Consensus , Deconstructed and Abstracted . In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing , Cham . 912\u2013939. \u00c1lvaro Garc\u00eda-P\u00e9rez, Alexey Gotsman, Yuri Meshman, and Ilya Sergey. 2018. Paxos Consensus, Deconstructed and Abstracted. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham. 912\u2013939."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409005"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_37_1","unstructured":"Hyperledger. 2021. The Hyperledger Project. https:\/\/www.hyperledger.org\/  Hyperledger. 2021. The Hyperledger Project. https:\/\/www.hyperledger.org\/"},{"key":"e_1_2_2_38_1","volume-title":"Better Verification Through Symmetry. Formal methods in system design, 9, 1-2","author":"Norris Ip C","year":"1996","unstructured":"C Norris Ip and David L Dill . 1996. Better Verification Through Symmetry. Formal methods in system design, 9, 1-2 ( 1996 ), 41\u201375. C Norris Ip and David L Dill. 1996. Better Verification Through Symmetry. Formal methods in system design, 9, 1-2 (1996), 41\u201375."},{"key":"e_1_2_2_39_1","volume-title":"Parameterized Verification of Systems with Global Synchronization and Guards","author":"Jaber Nouraldin","unstructured":"Nouraldin Jaber , Swen Jacobs , Christopher Wagner , Milind Kulkarni , and Roopsha Samanta . 2020. Parameterized Verification of Systems with Global Synchronization and Guards . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing , Cham . 299\u2013323. isbn:978-3-030-53288-8 Nouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni, and Roopsha Samanta. 2020. Parameterized Verification of Systems with Global Synchronization and Guards. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham. 299\u2013323. isbn:978-3-030-53288-8"},{"key":"e_1_2_2_40_1","volume-title":"Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613","author":"Jaber Nouraldin","year":"2020","unstructured":"Nouraldin Jaber , Christopher Wagner , Swen Jacobs , Milind Kulkarni , and Roopsha Samanta . 2020. Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613 ( 2020 ), arXiv:2004.04613. arxiv:2004.04613 Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, and Roopsha Samanta. 2020. Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613 (2020), arXiv:2004.04613. arxiv:2004.04613"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_12"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_2_2_43_1","volume-title":"Simon Oddershede Gregersen, and Lars Birkedal.","author":"Krogh-Jespersen Morten","year":"2020","unstructured":"Morten Krogh-Jespersen , Amin Timany , Marit Edna Ohlenbusch , Simon Oddershede Gregersen, and Lars Birkedal. 2020 . Aneris : A Mechanised Logic for Modular Reasoning about Distributed Systems. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing , Cham. 336\u2013365. isbn:978-3-030-44914-8 Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. 2020. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham. 336\u2013365. isbn:978-3-030-44914-8"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_2_45_1","volume-title":"Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","unstructured":"Leslie Lamport . 2002. Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. . Leslie Lamport. 2002. Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc.."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384645"},{"key":"e_1_2_2_49_1","volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","unstructured":"Nancy A. Lynch . 1996. Distributed Algorithms . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. isbn:1558603484 Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:1558603484"},{"key":"e_1_2_2_50_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Mao Yanhua","year":"2008","unstructured":"Yanhua Mao , Flavio P. Junqueira , and Keith Marzullo . 2008 . Mencius: Building Efficient Replicated State Machines for WANs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908) . USENIX Association, USA. 369\u2013384. https:\/\/doi.org\/10.5555\/ 1855741.1855767 10.5555\/1855741.1855767 Yanhua Mao, Flavio P. Junqueira, and Keith Marzullo. 2008. Mencius: Building Efficient Replicated State Machines for WANs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, USA. 369\u2013384. https:\/\/doi.org\/10.5555\/1855741.1855767"},{"key":"e_1_2_2_51_1","volume-title":"Cutoff Bounds for Consensus Algorithms. In International Conference on Computer Aided Verification. 217\u2013237","author":"Mari\u0107 Ognjen","year":"2017","unstructured":"Ognjen Mari\u0107 , Christoph Sprenger , and David Basin . 2017 . Cutoff Bounds for Consensus Algorithms. In International Conference on Computer Aided Verification. 217\u2013237 . Ognjen Mari\u0107, Christoph Sprenger, and David Basin. 2017. Cutoff Bounds for Consensus Algorithms. In International Conference on Computer Aided Verification. 217\u2013237."},{"key":"e_1_2_2_52_1","unstructured":"NASA. 2021. NASA - Small Aircraft Transportation System. https:\/\/www.nasa.gov\/centers\/langley\/news\/factsheets\/SATS.html  NASA. 2021. NASA - Small Aircraft Transportation System. https:\/\/www.nasa.gov\/centers\/langley\/news\/factsheets\/SATS.html"},{"key":"e_1_2_2_53_1","volume-title":"USENIX Annual Technical Conference. 305\u2013319","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\u2013319 . Diego Ongaro and John K Ousterhout. 2014. In Search of an Understandable Consensus Algorithm.. In USENIX Annual Technical Conference. 305\u2013319."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5501650"},{"key":"e_1_2_2_59_1","unstructured":"Vincent Rahli. 2012. Interfacing with Proof Assistants for Domain Specific Programming Using EventML.  Vincent Rahli. 2012. Interfacing with Proof Assistants for Domain Specific Programming Using EventML."},{"key":"e_1_2_2_60_1","unstructured":"RedisRaft. 2021. RedisRaft. https:\/\/github.com\/RedisLabs\/redisraft\/  RedisRaft. 2021. RedisRaft. https:\/\/github.com\/RedisLabs\/redisraft\/"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90211-6"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_2_2_66_1","volume-title":"Adaptive Symmetry Reduction. In International Conference on Computer Aided Verification. 393\u2013405","author":"Wahl Thomas","year":"2007","unstructured":"Thomas Wahl . 2007 . Adaptive Symmetry Reduction. In International Conference on Computer Aided Verification. 393\u2013405 . Thomas Wahl. 2007. Adaptive Symmetry Reduction. In International Conference on Computer Aided Verification. 393\u2013405."},{"key":"e_1_2_2_67_1","volume-title":"2nd Summit on Advances in Programming Languages (SNAPL","author":"Wilcox James R.","year":"2017","unstructured":"James R. Wilcox , Ilya Sergey , and Zachary Tatlock . 2017. Programming Language Abstractions for Modularly Verified Distributed Systems . In 2nd Summit on Advances in Programming Languages (SNAPL 2017 ), Benjamin S. Lerner, Rastislav Bod\u00edk , and Shriram Krishnamurthi (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs) , Vol. 71). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 19:1\u201319: 12 . isbn:978-3-95977-032-3 issn:1868-8969 James R. Wilcox, Ilya Sergey, and Zachary Tatlock. 2017. Programming Language Abstractions for Modularly Verified Distributed Systems. In 2nd Summit on Advances in Programming Languages (SNAPL 2017), Benjamin S. Lerner, Rastislav Bod\u00edk, and Shriram Krishnamurthi (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 71). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 19:1\u201319:12. isbn:978-3-95977-032-3 issn:1868-8969"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_2_70_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI\u201909)","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , and Lidong Zhou . 2009 . MODIST: Transparent Model Checking of Unmodified Distributed Systems . In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI\u201909) . USENIX Association, USA. 213\u2013228. Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI\u201909). USENIX Association, USA. 213\u2013228."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485534","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485534","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485534","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485534"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":70,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485534"],"URL":"https:\/\/doi.org\/10.1145\/3485534","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}