{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:25Z","timestamp":1775873665703,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"FP7 Ideas: European Research Council","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1655166"],"award-info":[{"award-number":["1655166"]}],"id":[{"id":"10.13039\/100000001","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":[[2017,10,12]]},"abstract":"<jats:p>Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve both quantifier alternations and higher-order concepts such as set cardinalities and arithmetic.<\/jats:p><jats:p>This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)\u2014a decidable fragment of first-order logic (also known as the Bernays-Sch\u00f6nfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos, Fast Paxos and Stoppable Paxos.<\/jats:p>","DOI":"10.1145\/3140568","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":75,"title":["Paxos made EPR: decidable reasoning about distributed protocols"],"prefix":"10.1145","volume":"1","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuliano","family":"Losa","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_6"},{"key":"e_1_2_1_2_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 171\u2013177","author":"Barrett Clark","year":"2011","unstructured":"Clark Barrett , Christopher L. Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovic , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011 . CVC4. In Computer Aided Verification - 23rd International Conference , CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 171\u2013177 . Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 171\u2013177."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11294-2_6"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"e_1_2_1_6_1","volume-title":"The Chubby Lock Service for Loosely-Coupled Distributed Systems. In 7th Symposium on Operating Systems Design and Implementation OSDI \u201906)","author":"Burrows Michael","year":"2006","unstructured":"Michael Burrows . 2006 . The Chubby Lock Service for Loosely-Coupled Distributed Systems. In 7th Symposium on Operating Systems Design and Implementation OSDI \u201906) , November 6-8, Seattle, WA, USA. USENIX Association, 335\u2013350. Michael Burrows. 2006. The Chubby Lock Service for Loosely-Coupled Distributed Systems. In 7th Symposium on Operating Systems Design and Implementation OSDI \u201906), November 6-8, Seattle, WA, USA. USENIX Association, 335\u2013350."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0084-6"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14808-8_3"},{"key":"e_1_2_1_10_1","volume-title":"Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016","author":"Chen Haogang","year":"2016","unstructured":"Haogang Chen , Daniel Ziegler , Tej Chajed , Adam Chlipala , M. Frans Kaashoek , and Nickolai Zeldovich . 2016 . Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016 , Denver, CO, USA , June 22-24, 2016. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2016. Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016, Denver, CO, USA, June 22-24, 2016."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503112.503113"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837650"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_17_1","volume-title":"Flexible Paxos: Quorum Intersection Revisited. arXiv preprint arXiv:1608.06696","author":"Howard Heidi","year":"2016","unstructured":"Heidi Howard , Dahlia Malkhi , and Alexander Spiegelman . 2016 . Flexible Paxos: Quorum Intersection Revisited. arXiv preprint arXiv:1608.06696 (2016). Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum Intersection Revisited. arXiv preprint arXiv:1608.06696 (2016)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_2_1_21_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . The MIT Press . Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press."},{"key":"e_1_2_1_22_1","volume-title":"Proving the Correctness of Disk Paxos. Archive of Formal Proofs (June","author":"Jaskelioff Mauro","year":"2005","unstructured":"Mauro Jaskelioff and Stephan Merz . 2005. Proving the Correctness of Disk Paxos. Archive of Formal Proofs (June 2005 ). http:\/\/isa- afp.org\/entries\/DiskPaxos.shtml , Formal proof development. Mauro Jaskelioff and Stephan Merz. 2005. Proving the Correctness of Disk Paxos. Archive of Formal Proofs (June 2005). http:\/\/isa- afp.org\/entries\/DiskPaxos.shtml , Formal proof development."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41579-6_2"},{"key":"e_1_2_1_26_1","volume-title":"4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298","author":"Korovin Konstantin","year":"2008","unstructured":"Konstantin Korovin . 2008 . iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Automated Reasoning , 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298 . Konstantin Korovin. 2008. iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_29_1","volume-title":"Paxos Made Simple. (December","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001. Paxos Made Simple. (December 2001 ), 51\u201358. https:\/\/www.microsoft.com\/en- us\/research\/publication\/ paxos- made- simple\/ Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51\u201358. https:\/\/www.microsoft.com\/en- us\/research\/publication\/ paxos- made- simple\/"},{"key":"e_1_2_1_30_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , Boston, MA, USA . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_2_1_32_1","unstructured":"Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. TechReport Microsoft Research. https:\/\/www.microsoft.com\/en- us\/research\/publication\/stoppable- paxos\/ Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. TechReport Microsoft Research. https:\/\/www.microsoft.com\/en- us\/research\/publication\/stoppable- paxos\/"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1582716.1582783"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1753171.1753191"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/383962.383969","article-title":"The ABCD\u2019s of Paxos","volume":"1","author":"Lampson Butler","year":"2001","unstructured":"Butler Lampson . 2001 . The ABCD\u2019s of Paxos . In PODC , Vol. 1. 13 . Butler Lampson. 2001. The ABCD\u2019s of Paxos. In PODC, Vol. 1. 13.","journal-title":"PODC"},{"key":"e_1_2_1_36_1","volume-title":"Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino . 2010 . Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning . Springer , 348\u2013370. K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348\u2013370."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886668"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_41_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic . Vol. 2283 . Springer Science & amp; Business Media. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Vol. 2283. Springer Science &amp; Business Media."},{"key":"e_1_2_1_42_1","volume-title":"2014 USENIX Annual Technical Conference, USENIX ATC \u201914","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John K. Ousterhout . 2014. In Search of an Understandable Consensus Algorithm . In 2014 USENIX Annual Technical Conference, USENIX ATC \u201914 , Philadelphia, PA, USA , June 19-20, 2014 . 305\u2013319. https:\/\/www.usenix.org\/ conference\/atc14\/technical- sessions\/presentation\/ongaro Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference, USENIX ATC \u201914, Philadelphia, PA, USA, June 19-20, 2014. 305\u2013319. https:\/\/www.usenix.org\/ conference\/atc14\/technical- sessions\/presentation\/ongaro"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357177"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_2_1_47_1","volume-title":"15th international workshop on automated verification of critical systems (avocs 2015","author":"Rahli Vincent","year":"2015","unstructured":"Vincent Rahli , David Guaspari , Mark Bickford , and Robert L. Constable . 2015 . 15th international workshop on automated verification of critical systems (avocs 2015 ). electronic communications of the easst 72 ( 2015 ). Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. 2015. 15th international workshop on automated verification of critical systems (avocs 2015). electronic communications of the easst 72 (2015)."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749613"},{"key":"e_1_2_1_49_1","first-page":"3","article-title":"The Design and Implementation of VAMPIRE","volume":"15","author":"Riazanov Alexandre","year":"2002","unstructured":"Alexandre Riazanov and Andrei Voronkov . 2002 . The Design and Implementation of VAMPIRE . AI Commun. 15 , 2, 3 (Aug. 2002), 91\u2013110. http:\/\/dl.acm.org\/citation.cfm?id=1218615.1218620 Alexandre Riazanov and Andrei Voronkov. 2002. The Design and Implementation of VAMPIRE. AI Commun. 15, 2,3 (Aug. 2002), 91\u2013110. http:\/\/dl.acm.org\/citation.cfm?id=1218615.1218620","journal-title":"AI Commun."},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"N. Schiper V. Rahli R. V. Renesse M. Bickford and R. L. Constable. 2014. developing correctly replicated databases using formal tools. In 2014 44th annual ieee\/ifip international conference on dependable systems and networks. 395\u2013406. N. Schiper V. Rahli R. V. Renesse M. Bickford and R. L. Constable. 2014. developing correctly replicated databases using formal tools. In 2014 44th annual ieee\/ifip international conference on dependable systems and networks. 395\u2013406.","DOI":"10.1109\/DSN.2014.45"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908129"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3140568","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3140568","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3140568","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:21Z","timestamp":1750212681000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3140568"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":54,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3140568"],"URL":"https:\/\/doi.org\/10.1145\/3140568","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}