{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T12:19:16Z","timestamp":1784204356519,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1901523"],"award-info":[{"award-number":["CNS-1901523"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2330066"],"award-info":[{"award-number":["2330066"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Google Ph.D. Fellowship"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,8]]},"DOI":"10.1145\/3718958.3750533","type":"proceedings-article","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T16:54:11Z","timestamp":1756313651000},"page":"409-433","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["ZENITH: Towards A Formally Verified Highly-Available Control Plane"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7704-5440","authenticated-orcid":false,"given":"Pooria","family":"Namyar","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8416-3297","authenticated-orcid":false,"given":"Arvin","family":"Ghavidel","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5352-413X","authenticated-orcid":false,"given":"Mingyang","family":"Zhang","sequence":"additional","affiliation":[{"name":"Google, Sunnyvale, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7978-9643","authenticated-orcid":false,"given":"Harsha V.","family":"Madhyastha","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2965-3940","authenticated-orcid":false,"given":"Srivatsan","family":"Ravi","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4684-3943","authenticated-orcid":false,"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8311-8853","authenticated-orcid":false,"given":"Ramesh","family":"Govindan","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, California, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. A High-Level View of TLA+. https:\/\/lamport.azurewebsites.net\/tla\/high-level-view.html. ([n. d.])."},{"key":"e_1_3_2_1_2_1","unstructured":"[n. d.]. MongoDB. https:\/\/www.mongodb.com\/. ([n. d.])."},{"key":"e_1_3_2_1_3_1","unstructured":"[n. d.]. ONOS Network Topology State Management. https:\/\/wiki.onosproject.org\/display\/ONOS\/Network+Topology+State. ([n. d.])."},{"key":"e_1_3_2_1_4_1","unstructured":"[n. d.]. OpenDaylight. https:\/\/www.opendaylight.org\/. ([n. d.])."},{"key":"e_1_3_2_1_5_1","unstructured":"[n. d.]. OpenDayLight Incident 1. https:\/\/git.opendaylight.org\/gerrit\/c\/controller\/+\/32352?usp=search. ([n. d.])."},{"key":"e_1_3_2_1_6_1","unstructured":"[n. d.]. OpenDayLight Incident 2. https:\/\/git.opendaylight.org\/gerrit\/c\/bgpcep\/+\/33697?usp=search. ([n. d.])."},{"key":"e_1_3_2_1_7_1","unstructured":"[n. d.]. The Sphere Testbed Platform. https:\/\/sphere-project.net\/. ([n. d.])."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Parosh Abdulla Stavros Aronis Bengt Jonsson and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. SIGPLAN Not. (2014).","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359664"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472912"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2620728.2620744"},{"key":"e_1_3_2_1_13_1","volume-title":"10th International Conference, CAV.","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. 1998. Symmetry Reductions in Model Checking. In Computer Aided Verification, 10th International Conference, CAV."},{"key":"e_1_3_2_1_14_1","volume-title":"Long","author":"Clarke Edmund M.","year":"1994","unstructured":"Edmund M. Clarke, Orna Grumberg, and David E. Long. 1994. Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. (1994)."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89)","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. 1989. Compositional Model Checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89)."},{"key":"e_1_3_2_1_16_1","volume-title":"arXiv:1208.5933","author":"Cousineau Denis","year":"2012","unstructured":"Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hern\u00e1n Vanzetto. 2012. TLA+ Proofs. (2012). arXiv:1208.5933"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774993.2774999"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908124"},{"key":"e_1_3_2_1_19_1","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Ferguson Andrew D.","year":"2021","unstructured":"Andrew D. Ferguson, Steve Gribble, Chi-Yao Hong, Charles Killian, Waqar Mohsin, Henrik Muehe, Joon Ong, Leon Poutievski, Arjun Singh, Lorenzo Vicisano, Richard Alimi, Shawn Shuoshuo Chen, Mike Conley, Subhasree Mandal, Karthik Nagaraj, Kondapa Naidu Bollineni, Amr Sabaa, Shidong Zhang, Min Zhu, and Amin Vahdat. 2021. Orion: Google's Software-Defined Networking Control Plane. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)."},{"key":"e_1_3_2_1_20_1","volume-title":"12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)","author":"Fogel Ari","year":"2015","unstructured":"Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Klaus-Tycho F\u00f6rster Ratul Mahajan and Roger Wattenhofer. 2016. Consistent Updates in Software Defined Networks: On Dependencies Loop Freedom and Blackholes. In IFIP NETWORKING.","DOI":"10.1109\/IFIPNetworking.2016.7497232"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Phillipa Gill Navendu Jain and Nachiappan Nagappan. 2011. Understanding Network Failures in Data Centers: Measurement Analysis and Implications. SIGCOMM Comput. Commun. Rev. (2011).","DOI":"10.1145\/2018436.2018477"},{"key":"e_1_3_2_1_23_1","volume-title":"2nd International Workshop, CAV '90","author":"Godefroid Patrice","year":"1990","unstructured":"Patrice Godefroid. 1990. Using Partial Orders to Improve Automatic Verification Methods. In Computer Aided Verification, 2nd International Workshop, CAV '90."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934891"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575695"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles (SOSP '15)","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP '15). Association for Computing Machinery."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"S. Henry and D. Kafura. 1981. Software Structure Metrics Based on Information Flow. IEEE Transactions on Software Engineering (1981).","DOI":"10.1109\/TSE.1981.231113"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230545"},{"key":"e_1_3_2_1_29_1","volume-title":"B4: Experience with a Globally-deployed Software Defined Wan. SIGCOMM CCR","author":"Jain Sushant","year":"2013","unstructured":"Sushant Jain, Alok Kumar, Subhasree Mandal, Joon Ong, Leon Poutievski, Arjun Singh, Subbaiah Venkata, Jim Wanderer, Junlan Zhou, Min Zhu, Jon Zolla, Urs H\u00f6lzle, Stephen Stuart, and Amin Vahdat. 2013. B4: Experience with a Globally-deployed Software Defined Wan. SIGCOMM CCR (2013)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626307"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774993.2774996"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation (OSDI'10)","author":"Koponen Teemu","year":"2010","unstructured":"Teemu Koponen, Martin Casado, Natasha Gude, Jeremy Stribling, Leon Poutievski, Min Zhu, Rajiv Ramanathan, Yuichiro Iwata, Hiroaki Inoue, Takayuki Hama, and Scott Shenker. 2010. Onix: a distributed control platform for large-scale production networks. In Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation (OSDI'10). USENIX Association."},{"key":"e_1_3_2_1_34_1","volume-title":"20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Krishnaswamy Umesh","year":"2023","unstructured":"Umesh Krishnaswamy, Rachee Singh, Paul Mattes, Paul-Andre C Bissonnette, Nikolaj Bj\u00f8rner, Zahira Nasrin, Sonal Kothari, Prabhakar Reddy, John Abeln, Srikanth Kandula, Himanshu Raj, Luis Irun-Briz, Jamie Gaudette, and Erica Lan. 2023. OneWAN is better than two: Unifying a split WAN architecture. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23). USENIX Association."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Leslie Lamport. 1994. The temporal logic of actions. ACM Trans. Program. Lang. Syst. (1994).","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075029.2075058"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the Fourteenth EuroSys Conference 2019 (EuroSys '19)","author":"Lukman Jeffrey F.","unstructured":"Jeffrey F. Lukman, Huan Ke, Cesar A. Stuardo, Riza O. Suminto, Daniar H. Kurniawan, Dikaimin Simon, Satria Priambada, Chen Tian, Feng Ye, Tanakorn Leesatapornwongsa, Aarti Gupta, Shan Lu, and Haryadi S. Gunawi. 2019. FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems. In Proceedings of the Fourteenth EuroSys Conference 2019 (EuroSys '19). Association for Computing Machinery."},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the Symposium on SDN Research (SOSR '17)","author":"May Roman","year":"2017","unstructured":"Roman May, Ahmed El-Hassany, Laurent Vanbever, and Martin Vechev. 2017. BigBug: Practical Concurrency Analysis for SDN. In Proceedings of the Symposium on SDN Research (SOSR '17). Association for Computing Machinery."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Jedidiah McClurg Hossein Hojjat Nate Foster and Pavol \u010cern\u1ef3. 2016. Event-driven Network Programming. In SIGPLAN Notices.","DOI":"10.1145\/2908080.2908097"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Nick McKeown Tom Anderson Hari Balakrishnan Guru Parulkar Larry Peterson Jennifer Rexford Scott Shenker and Jonathan Turner. 2008. OpenFlow: Enabling Innovation in Campus Networks. SIGCOMM Comput. Commun. Rev. (2008).","DOI":"10.1145\/1355734.1355746"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/3691825.3691877"},{"key":"e_1_3_2_1_42_1","volume-title":"Solving Max-Min Fair Resource Allocations Quickly on Large Graphs. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Namyar Pooria","year":"2024","unstructured":"Pooria Namyar, Behnaz Arzani, Srikanth Kandula, Santiago Segarra, Daniel Crankshaw, Umesh Krishnaswamy, Ramesh Govindan, and Himanshu Raj. 2024. Solving Max-Min Fair Resource Allocations Quickly on Large Graphs. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)."},{"key":"e_1_3_2_1_43_1","volume-title":"Enhancing Network Failure Mitigation with Performance-Aware Ranking. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25)","author":"Namyar Pooria","year":"2025","unstructured":"Pooria Namyar, Arvin Ghavidel, Daniel Crankshaw, Daniel S. Berger, Kevin Hsieh, Srikanth Kandula, Ramesh Govindan, and Behnaz Arzani. 2025. Enhancing Network Failure Mitigation with Performance-Aware Ranking. In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25). USENIX Association."},{"key":"e_1_3_2_1_44_1","volume-title":"How Amazon web services uses formal methods. Commun. ACM","author":"Newcombe Chris","year":"2015","unstructured":"Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. How Amazon web services uses formal methods. Commun. ACM (2015)."},{"key":"e_1_3_2_1_45_1","volume-title":"SCL: Simplifying Distributed SDN Control Planes. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Panda Aurojit","year":"2017","unstructured":"Aurojit Panda, Wenting Zheng, Xiaohe Hu, Arvind Krishnamurthy, and Scott Shenker. 2017. SCL: Simplifying Distributed SDN Control Planes. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association."},{"key":"e_1_3_2_1_46_1","volume-title":"5th International Conference, CAV '93","author":"Peled Doron A.","year":"1993","unstructured":"Doron A. Peled. 1993. All from One, One for All: on Model Checking Using Representatives. In Computer Aided Verification, 5th International Conference, CAV '93."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342427"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Natali Ruchansky and Davide Proserpio. 2013. A (not) NICE way to verify the openflow switch specification: formal modelling of the openflow switch using alloy. SIGCOMM Comput. Commun. Rev. (2013).","DOI":"10.1145\/2486001.2491711"},{"key":"e_1_3_2_1_49_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Ryzhyk Leonid","year":"2017","unstructured":"Leonid Ryzhyk, Nikolaj Bj\u00f8rner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese. 2017. Correct by Construction Networks Using Stepwise Refinement. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)."},{"key":"e_1_3_2_1_50_1","volume-title":"2018 14th International Conference on Advanced Trends in Radioelecrtronics, Telecommunications and Computer Engineering (TCSET).","author":"Shkarupylo Vadym","year":"2018","unstructured":"Vadym Shkarupylo and Olga Polska. 2018. The approach to SDN Network topology verification on a basis of Temporal Logic of Actions. In 2018 14th International Conference on Advanced Trends in Radioelecrtronics, Telecommunications and Computer Engineering (TCSET)."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787508"},{"key":"e_1_3_2_1_52_1","volume-title":"Proceedings of the 16th ACM Workshop on Hot Topics in Networks (HotNets '17)","author":"Singh Rachee","year":"2017","unstructured":"Rachee Singh, Monia Ghobadi, Klaus-Tycho Foerster, Mark Filer, and Phillipa Gill. 2017. Run, Walk, Crawl: Towards Dynamic Link Capacities. In Proceedings of the 16th ACM Workshop on Hot Topics in Networks (HotNets '17). Association for Computing Machinery."},{"key":"e_1_3_2_1_53_1","volume-title":"Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"},{"key":"e_1_3_2_1_55_1","volume-title":"11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14)","author":"Zeng Hongyi","year":"2014","unstructured":"Hongyi Zeng, Shidong Zhang, Fei Ye, Vimalkumar Jeyakumar, Mickey Ju, Junda Liu, Nick McKeown, and Amin Vahdat. 2014. Libra: Divide and Conquer to Verify Forwarding Tables in Huge Networks. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14). USENIX Association."},{"key":"e_1_3_2_1_56_1","volume-title":"Proc. 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI","author":"Zhao Shizhen","year":"2019","unstructured":"Shizhen Zhao, Rui Wang, Junlan Zhou, Joon Ong, Jeffrey C. Mogul, and Amin Vahdat. 2019. Minimal Rewiring: Efficient Live Expansion for Clos Data Center Networks. In Proc. 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2019)."},{"key":"e_1_3_2_1_57_1","unstructured":"Wenxuan Zhou Dong Jin Jason Croft Matthew Caesar and P. Brighten Godfrey. 2015. Enforcing Customizable Consistency Properties in Software-defined Networks. In NSDI. 73\u201385."}],"event":{"name":"SIGCOMM '25: ACM SIGCOMM 2025 Conference","location":"S\u00e3o Francisco Convent Coimbra Portugal","acronym":"SIGCOMM '25","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2025 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3718958.3750533","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T17:01:38Z","timestamp":1756314098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3718958.3750533"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,27]]},"references-count":57,"alternative-id":["10.1145\/3718958.3750533","10.1145\/3718958"],"URL":"https:\/\/doi.org\/10.1145\/3718958.3750533","relation":{},"subject":[],"published":{"date-parts":[[2025,8,27]]},"assertion":[{"value":"2025-08-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}