{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:06:47Z","timestamp":1750309607002,"version":"3.41.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Union's Horizon 2020 research and innovation programme","award":["759102-SVIS,"],"award-info":[{"award-number":["759102-SVIS,"]}]},{"name":"Israeli Science Foundation","award":["1810\/18"],"award-info":[{"award-number":["1810\/18"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Formally verifying infinite-state systems can be a daunting task, especially when it comes to reasoning about quantifiers. In particular, quantifier alternations in conjunction with function symbols can create function cycles that result in infinitely many ground terms, making it difficult for solvers to instantiate quantifiers and causing them to diverge. This can  \nleave users with no useful information on how to proceed.  \n\t\t  \nTo address this issue, we propose an interactive verification methodology that uses a relational abstraction technique to mitigate solver divergence in the presence of quantifiers. This technique abstracts functions in the verification conditions (VCs) as one-to-one relations, which avoids the creation of function cycles and the resulting proliferation of ground terms.  \n\t\t  \nRelational abstraction is sound and guarantees correctness if the solver cannot find counter-models. However, it may also lead to false counterexamples, which can be addressed by refining the abstraction and requiring the existence of corresponding elements.  \nIn the domain of distributed protocols, we can refine the abstraction by diagnosing counterexamples and manually instantiating elements in the range of the original function. If the verification conditions are correct, there always exist finitely many refinement steps that eliminate all spurious counter-models, making the approach complete.  \n\t\t  \nWe applied this approach in Ivy to verify the safety properties of consensus protocols and found that: (1) most verification goals can be automatically verified using relational abstraction, while SMT solvers often diverge when given the original VC, (2) only a few manual instantiations were needed, and the counterexamples provided valuable guidance for the user  \ncompared to timeouts produced by the traditional approach, and (3) the technique can be used to derive efficient low-level implementations of tricky algorithms.<\/jats:p>","DOI":"10.1145\/3622864","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1878-1904","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9788-5523","authenticated-orcid":false,"given":"Orr","family":"Tamir","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1002-0662","authenticated-orcid":false,"given":"Marcelo","family":"Taube","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4389-7471","authenticated-orcid":false,"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, Bellevue, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9149-8080","authenticated-orcid":false,"given":"Guy","family":"Gueta","sequence":"additional","affiliation":[{"name":"VMware Research, Herzliya, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0723-1309","authenticated-orcid":false,"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Sync HotStuff: Simple and Practical Synchronous State Machine Replication. In 2020 IEEE Symposium on Security and Privacy, SP 2020","author":"Abraham Ittai","year":"2020","unstructured":"Ittai Abraham , Dahlia Malkhi , Kartik Nayak , Ling Ren , and Maofan Yin . 2020 . Sync HotStuff: Simple and Practical Synchronous State Machine Replication. In 2020 IEEE Symposium on Security and Privacy, SP 2020 , San Francisco, CA, USA , May 18-21, 2020. IEEE, 106\u2013118. Ittai Abraham, Dahlia Malkhi, Kartik Nayak, Ling Ren, and Maofan Yin. 2020. Sync HotStuff: Simple and Practical Synchronous State Machine Replication. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020. IEEE, 106\u2013118."},{"key":"e_1_2_1_2_1","volume-title":"17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, David A. McAllester (Ed.) (Lecture Notes in Computer Science","volume":"176","author":"Allen Stuart F.","year":"2000","unstructured":"Stuart F. Allen , Robert L. Constable , Richard Eaton , Christoph Kreitz , and Lori Lorigo . 2000 . The Nuprl Open Logical Environment. In Automated Deduction - CADE-17 , 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, David A. McAllester (Ed.) (Lecture Notes in Computer Science , Vol. 1831). Springer, 170\u2013 176 . Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. 2000. The Nuprl Open Logical Environment. In Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, David A. McAllester (Ed.) (Lecture Notes in Computer Science, Vol. 1831). Springer, 170\u2013176."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"e3","DOI":"10.1017\/S095679682000026X","article-title":"Protocol combinators for modeling, testing, and execution of distributed systems","volume":"31","author":"Arndal Andersen Kristoffer Just","year":"2021","unstructured":"Kristoffer Just Arndal Andersen and Ilya Sergey . 2021 . Protocol combinators for modeling, testing, and execution of distributed systems . J. Funct. Program. , 31 (2021), e3 . Kristoffer Just Arndal Andersen and Ilya Sergey. 2021. Protocol combinators for modeling, testing, and execution of distributed systems. J. Funct. Program., 31 (2021), e3.","journal-title":"J. Funct. Program."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.028"},{"key":"e_1_2_1_5_1","volume-title":"NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Julia M. Badger and Kristin Yvonne Rozier (Eds.) (Lecture Notes in Computer Science","volume":"53","author":"Ashmore Rylo","unstructured":"Rylo Ashmore , Arie Gurfinkel , and Richard J. Trefler . 2019. Local Reasoning for Parameterized First Order Protocols. In NASA Formal Methods - 11th International Symposium , NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Julia M. Badger and Kristin Yvonne Rozier (Eds.) (Lecture Notes in Computer Science , Vol. 11460). Springer, 36\u2013 53 . Rylo Ashmore, Arie Gurfinkel, and Richard J. Trefler. 2019. Local Reasoning for Parameterized First Order Protocols. In NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Julia M. Badger and Kristin Yvonne Rozier (Eds.) (Lecture Notes in Computer Science, Vol. 11460). Springer, 36\u201353."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_1_7_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science","volume":"105","author":"Bansal Kshitij","year":"2015","unstructured":"Kshitij Bansal , Andrew Reynolds , Tim King , Clark W. Barrett , and Thomas Wies . 2015 . Deciding Local Theory Extensions via E-matching. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science , Vol. 9207). Springer, 87\u2013 105 . Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, and Thomas Wies. 2015. Deciding Local Theory Extensions via E-matching. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science, Vol. 9207). Springer, 87\u2013105."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_6"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 2011 IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2011","author":"Bokor P\u00e9ter","year":"2011","unstructured":"P\u00e9ter Bokor , Johannes Kinder , Marco Serafini , and Neeraj Suri . 2011 . Efficient model checking of fault-tolerant distributed protocols . In Proceedings of the 2011 IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2011 , Hong Kong, China , June 27-30 2011. IEEE Compute Society, 73\u201384. P\u00e9ter Bokor, Johannes Kinder, Marco Serafini, and Neeraj Suri. 2011. Efficient model checking of fault-tolerant distributed protocols. In Proceedings of the 2011 IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2011, Hong Kong, China, June 27-30 2011. IEEE Compute Society, 73\u201384."},{"key":"e_1_2_1_10_1","first-page":"195","article-title":"On Herbrand\u2019s Theorem. In Logic and Computational Complexity","volume":"960","author":"Buss Samuel R.","year":"1995","unstructured":"Samuel R. Buss . 1995 . On Herbrand\u2019s Theorem. In Logic and Computational Complexity , Lecture Notes in Computer Science , 960 (1995), 195 \u2013 209 . Samuel R. Buss. 1995. On Herbrand\u2019s Theorem. In Logic and Computational Complexity, Lecture Notes in Computer Science, 960 (1995), 195\u2013209.","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_2_1_11_1","unstructured":"Miguel Castro and Barbara Liskov. 1999. MIT. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/01\/tm590.pdf. \t\t\t\t  Miguel Castro and Barbara Liskov. 1999. MIT. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/01\/tm590.pdf."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/571637.571640"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_14_1","unstructured":"Nicolas T. Courtois Louis Goubin and Jacques Patarin. 2003. SFLASHv3 a fast asymmetric signature scheme. IACR Cryptol. ePrint Arch. 211. http:\/\/eprint.iacr.org\/2003\/211 \t\t\t\t  Nicolas T. Courtois Louis Goubin and Jacques Patarin. 2003. SFLASHv3 a fast asymmetric signature scheme. IACR Cryptol. ePrint Arch. 211. http:\/\/eprint.iacr.org\/2003\/211"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. \t\t\t\t  Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_16_1","volume-title":"Proc. ACM Program. Lang., 2, OOPSLA","author":"Desai Ankush","year":"2018","unstructured":"Ankush Desai , Amar Phanishayee , Shaz Qadeer , and Sanjit A. Seshia . 2018. Compositional programming and testing of dynamic distributed systems . Proc. ACM Program. Lang., 2, OOPSLA ( 2018 ), 159:1\u2013159:30. Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. 2018. Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang., 2, OOPSLA (2018), 159:1\u2013159:30."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St","author":"Dragoi Cezara","year":"2016","unstructured":"Cezara Dragoi , Thomas A. Henzinger , and Damien Zufferey . 2016 . PSync: a partially synchronous language for fault-tolerant distributed algorithms . In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St . Petersburg, FL, USA, January 20 - 22 , 2016, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM, 400\u2013415. Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bod\u00edk and Rupak Majumdar (Eds.). ACM, 400\u2013415."},{"key":"e_1_2_1_18_1","volume-title":"21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (Lecture Notes in Computer Science","volume":"320","author":"Ge Yeting","year":"2009","unstructured":"Yeting Ge and Leonardo de Moura . 2009 . Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories. In Computer Aided Verification , 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (Lecture Notes in Computer Science , Vol. 5643). Springer, 306\u2013 320 . Yeting Ge and Leonardo de Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5643). Springer, 306\u2013320."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_21_1","volume-title":"Flexible Paxos: Quorum intersection revisited. CoRR, abs\/1608.06696","author":"Howard Heidi","year":"2016","unstructured":"Heidi Howard , Dahlia Malkhi , and Alexander Spiegelman . 2016 . Flexible Paxos: Quorum intersection revisited. CoRR, abs\/1608.06696 (2016), arXiv:1608.06696. arxiv:1608.06696 Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum intersection revisited. CoRR, abs\/1608.06696 (2016), arXiv:1608.06696. arxiv:1608.06696"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"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.1145\/3009837.3009860"},{"key":"e_1_2_1_25_1","volume-title":"Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Paxos Made Simple, Fast, and Byzantine . In Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002 , Reims, France , December 11-13, 2002, Alain Bui and Hac\u00e8ne Fouchal (Eds.) (Studia Informatica Universalis, Vol. 3). Suger, Saint-Denis, rue Catulienne, France, 7\u20139. Leslie Lamport. 2002. Paxos Made Simple, Fast, and Byzantine. In Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002, Reims, France, December 11-13, 2002, Alain Bui and Hac\u00e8ne Fouchal (Eds.) (Studia Informatica Universalis, Vol. 3). Suger, Saint-Denis, rue Catulienne, France, 7\u20139."},{"key":"e_1_2_1_26_1","volume-title":"Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Paxos Made Simple, Fast, and Byzantine . In Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002 , Reims, France , December 11-13, 2002, Alain Bui and Hac\u00e8ne Fouchal (Eds.) (Studia Informatica Universalis, Vol. 3). Suger, Saint-Denis, rue Catulienne, France, 7\u20139. Leslie Lamport. 2002. Paxos Made Simple, Fast, and Byzantine. In Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002, Reims, France, December 11-13, 2002, Alain Bui and Hac\u00e8ne Fouchal (Eds.) (Studia Informatica Universalis, Vol. 3). Suger, Saint-Denis, rue Catulienne, France, 7\u20139."},{"volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","key":"e_1_2_1_27_1","unstructured":"Leslie Lamport . 2002. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1582716.1582783"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_2_1_30_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science","volume":"381","author":"K. Rustan","unstructured":"K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science , Vol. 9779). Springer, 361\u2013 381 . K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science, Vol. 9779). Springer, 361\u2013381."},{"key":"e_1_2_1_31_1","volume-title":"Chapar: Certified Causally Consistent Distributed Key-Value Stores. In POPL\u201916: Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Lesani Mohsen","year":"2016","unstructured":"Mohsen Lesani , Christian J. Bell , and Adam Chlipala . 2016 . Chapar: Certified Causally Consistent Distributed Key-Value Stores. In POPL\u201916: Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . http:\/\/adam.chlipala.net\/papers\/ChaparPOPL16\/ Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar: Certified Causally Consistent Distributed Key-Value Stores. In POPL\u201916: Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. http:\/\/adam.chlipala.net\/papers\/ChaparPOPL16\/"},{"key":"e_1_2_1_32_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"L\u00f6ding Christof","year":"2018","unstructured":"Christof L\u00f6ding , P. Madhusudan , and Lucas Pe\u00f1a . 2018 . Foundations for natural proofs and quantifier instantiation . Proc. ACM Program. Lang., 2, POPL (2018), 10:1\u201310:30. Christof L\u00f6ding, P. Madhusudan, and Lucas Pe\u00f1a. 2018. Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang., 2, POPL (2018), 10:1\u201310:30."},{"key":"e_1_2_1_33_1","unstructured":"Kenneth McMillan. 2020. Ivy. \t\t\t\t  Kenneth McMillan. 2020. Ivy."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"e_1_2_1_35_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 , Garth Gibson and Nickolai Zeldovich (Eds.). USENIX Association, 305\u2013319. 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, Garth Gibson and Nickolai Zeldovich (Eds.). USENIX Association, 305\u2013319."},{"key":"e_1_2_1_36_1","volume-title":"Proc. ACM Program. Lang., 1, OOPSLA","author":"Padon Oded","year":"2017","unstructured":"Oded Padon , Giuliano Losa , Mooly Sagiv , and Sharon Shoham . 2017 . Paxos made EPR: decidable reasoning about distributed protocols . Proc. ACM Program. Lang., 1, OOPSLA (2017), 108:1\u2013108:31. Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang., 1, OOPSLA (2017), 108:1\u2013108:31."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.009"},{"key":"e_1_2_1_40_1","volume-title":"ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 619\u2013650","author":"Rahli Vincent","year":"2018","unstructured":"Vincent Rahli , Ivana Vukotic , Marcus V\u00f6lp , and Paulo Jorge Esteves Ver\u00edssimo . 2018 . Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming , ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 619\u2013650 . Vincent Rahli, Ivana Vukotic, Marcus V\u00f6lp, and Paulo Jorge Esteves Ver\u00edssimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 619\u2013650."},{"key":"e_1_2_1_41_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Sergey Ilya","year":"2018","unstructured":"Ilya Sergey , James R. Wilcox , and Zachary Tatlock . 2018 . Programming and proving with distributed protocols . Proc. ACM Program. Lang., 2, POPL (2018), 28:1\u201328:30. Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. Proc. ACM Program. Lang., 2, POPL (2018), 28:1\u201328:30."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622864","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":43,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622864"],"URL":"https:\/\/doi.org\/10.1145\/3622864","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}