{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T14:58:04Z","timestamp":1784300284683,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T00:00:00Z","timestamp":1641859200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,1,17]]},"DOI":"10.1145\/3497775.3503688","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T05:20:48Z","timestamp":1641964848000},"page":"143-152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Formal verification of a distributed dynamic reconfiguration protocol"],"prefix":"10.1145","author":[{"given":"William","family":"Schultz","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Dardik","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Marcos Aguilera Idit Keidar Dahlia Malkhi Jean-Philippe Martin and Alexander Shraer. 2010. Reconfiguring Replicated Atomic Storage: A Tutorial. Bulletin of the European Association for Theoretical Computer Science EATCS.  Marcos Aguilera Idit Keidar Dahlia Malkhi Jean-Philippe Martin and Alexander Shraer. 2010. Reconfiguring Replicated Atomic Storage: A Tutorial. Bulletin of the European Association for Theoretical Computer Science EATCS."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33600-8_5"},{"key":"e_1_3_2_1_3_1","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions . Springer Science & Business Media . Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491245"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"e_1_3_2_1_14_1","volume-title":"Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21) . USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.14778\/3415478.3415535"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360549"},{"key":"e_1_3_2_1_18_1","volume-title":"How to write a proof. The American mathematical monthly, 102, 7","author":"Lamport Leslie","year":"1995","unstructured":"Leslie Lamport . 1995. How to write a proof. The American mathematical monthly, 102, 7 ( 1995 ), 600\u2013608. Leslie Lamport. 1995. How to write a proof. The American mathematical monthly, 102, 7 (1995), 600\u2013608."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_20_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 . Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24100-0_22"},{"key":"e_1_3_2_1_22_1","unstructured":"Leslie Lamport. 2018. Using TLC to Check Inductive Invariance. https:\/\/lamport.azurewebsites.net\/tla\/inductive-invariant.pdf  Leslie Lamport. 2018. Using TLC to Check Inductive Invariance. https:\/\/lamport.azurewebsites.net\/tla\/inductive-invariant.pdf"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319317"},{"key":"e_1_3_2_1_24_1","volume-title":"Temporal verification of reactive systems: safety","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 2012. Temporal verification of reactive systems: safety . Springer Science & Business Media . Zohar Manna and Amir Pnueli. 2012. Temporal verification of reactive systems: safety. Springer Science & Business Media."},{"key":"e_1_3_2_1_25_1","unstructured":"2021. MongoDB Github Project. https:\/\/github.com\/mongodb\/mongo  2021. MongoDB Github Project. https:\/\/github.com\/mongodb\/mongo"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_3_2_1_27_1","unstructured":"Diego Ongaro. 2014. Consensus: Bridging Theory and Practice. Doctoral thesis.  Diego Ongaro. 2014. Consensus: Bridging Theory and Practice. Doctoral thesis."},{"key":"e_1_3_2_1_28_1","unstructured":"Diego Ongaro. 2015. Bug in single-server membership changes. https:\/\/groups.google.com\/g\/raft-dev\/c\/t4xj6dJTP6E\/m\/d2D9LrWRza8J  Diego Ongaro. 2015. Bug in single-server membership changes. https:\/\/groups.google.com\/g\/raft-dev\/c\/t4xj6dJTP6E\/m\/d2D9LrWRza8J"},{"key":"e_1_3_2_1_29_1","volume-title":"2014 USENIX Annual Technical Conference (USENIX ATC 14)","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout . 2014 . In Search of an Understandable Consensus Algorithm . In 2014 USENIX Annual Technical Conference (USENIX ATC 14) . USENIX Association, Philadelphia, PA. 305\u2013319. isbn:978-1-93 1971-10-2 https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/ongaro Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference (USENIX ATC 14). USENIX Association, Philadelphia, PA. 305\u2013319. isbn:978-1-931971-10-2 https:\/\/www.usenix.org\/conference\/atc14\/technical-sessions\/presentation\/ongaro"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_34_1","volume-title":"Designing Distributed Systems Using Approximate Synchrony in Data Center Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)","author":"Ports Dan R. K.","year":"2015","unstructured":"Dan R. K. Ports , Jialin Li , Vincent Liu , Naveen Kr. Sharma , and Arvind Krishnamurthy . 2015 . Designing Distributed Systems Using Approximate Synchrony in Data Center Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15) . USENIX Association, Oakland, CA. 43\u201357. isbn:978-1-93 1971-218 https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/ports Dan R. K. Ports, Jialin Li, Vincent Liu, Naveen Kr. Sharma, and Arvind Krishnamurthy. 2015. Designing Distributed Systems Using Approximate Synchrony in Data Center Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association, Oakland, CA. 43\u201357. isbn:978-1-931971-218 https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/ports"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/98163.98167"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.14778\/3352063.3352125"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5768484"},{"key":"e_1_3_2_1_38_1","volume-title":"25th International Conference on Principles of Distributed Systems (OPODIS 2021), Quentin Bramas, Vincent Gramoli, and Alessia Milani (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs)","author":"Schultz William","year":"2022","unstructured":"William Schultz , Siyuan Zhou , Ian Dardik , and Stavros Tripakis . 2022 . Design and Analysis of a Logless Dynamic Reconfiguration Protocol . In 25th International Conference on Principles of Distributed Systems (OPODIS 2021), Quentin Bramas, Vincent Gramoli, and Alessia Milani (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs) , Vol. 217). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany. William Schultz, Siyuan Zhou, Ian Dardik, and Stavros Tripakis. 2022. Design and Analysis of a Logless Dynamic Reconfiguration Protocol. In 25th International Conference on Principles of Distributed Systems (OPODIS 2021), Quentin Bramas, Vincent Gramoli, and Alessia Milani (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 217). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany."},{"key":"e_1_3_2_1_39_1","volume-title":"Dynamic Reconfiguration of Primary\/Backup Clusters. In 2012 USENIX Annual Technical Conference (USENIX ATC 12)","author":"Shraer Alexander","year":"1971","unstructured":"Alexander Shraer , Benjamin Reed , Dahlia Malkhi , and Flavio P. Junqueira . 2012 . Dynamic Reconfiguration of Primary\/Backup Clusters. In 2012 USENIX Annual Technical Conference (USENIX ATC 12) . USENIX Association, Boston, MA. 425\u2013437. isbn:978-93 1971 -93-5 https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/shraer Alexander Shraer, Benjamin Reed, Dahlia Malkhi, and Flavio P. Junqueira. 2012. Dynamic Reconfiguration of Primary\/Backup Clusters. In 2012 USENIX Annual Technical Conference (USENIX ATC 12). USENIX Association, Boston, MA. 425\u2013437. isbn:978-931971-93-5 https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/shraer"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2019.105901"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318464.3386134"},{"key":"e_1_3_2_1_42_1","volume-title":"The origin of quorum systems. Bulletin of EATCS, 2, 101","author":"Vukoli\u0107 Marko","year":"2013","unstructured":"Marko Vukoli\u0107 . 2013. The origin of quorum systems. Bulletin of EATCS, 2, 101 ( 2013 ). Marko Vukoli\u0107. 2013. The origin of quorum systems. Bulletin of EATCS, 2, 101 (2013)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_1_45_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , Jason Nieh , Suman Jana , and Gabriel Ryan . 2021 . DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21) . USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"},{"key":"e_1_3_2_1_46_1","volume-title":"Model Checking TLA+ Specifications","author":"Yu Yuan","unstructured":"Yuan Yu , Panagiotis Manolios , and Leslie Lamport . 1999. Model Checking TLA+ Specifications . In Correct Hardware Design and Verification Methods, Laurence Pierre and Thomas Kropf (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 54\u201366. isbn:978-3-540-48153-9 Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model Checking TLA+ Specifications. In Correct Hardware Design and Verification Methods, Laurence Pierre and Thomas Kropf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 54\u201366. isbn:978-3-540-48153-9"},{"key":"e_1_3_2_1_47_1","volume-title":"Fault-Tolerant Replication with Pull-Based Consensus in MongoDB. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Zhou Siyuan","year":"2021","unstructured":"Siyuan Zhou and Shuai Mu . 2021 . Fault-Tolerant Replication with Pull-Based Consensus in MongoDB. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21) . USENIX Association, 687\u2013703. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/zhou Siyuan Zhou and Shuai Mu. 2021. Fault-Tolerant Replication with Pull-Based Consensus in MongoDB. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 687\u2013703. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/zhou"}],"event":{"name":"CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Philadelphia PA USA","acronym":"CPP '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503688","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3497775.3503688","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:25Z","timestamp":1750193365000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503688"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,11]]},"references-count":47,"alternative-id":["10.1145\/3497775.3503688","10.1145\/3497775"],"URL":"https:\/\/doi.org\/10.1145\/3497775.3503688","relation":{},"subject":[],"published":{"date-parts":[[2022,1,11]]},"assertion":[{"value":"2022-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}