{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T06:31:35Z","timestamp":1783146695802,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":94,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Key R&D Program of China","award":["2022YFB2901502"],"award-info":[{"award-number":["2022YFB2901502"]}]},{"name":"NSFC","award":["62172345"],"award-info":[{"award-number":["62172345"]}]},{"name":"NSFC","award":["62141220"],"award-info":[{"award-number":["62141220"]}]},{"name":"NSFC","award":["61972253"],"award-info":[{"award-number":["61972253"]}]},{"name":"NSFC","award":["U1908212"],"award-info":[{"award-number":["U1908212"]}]},{"name":"Open Research Projects of Zhejiang Lab","award":["2022QA0AB05"],"award-info":[{"award-number":["2022QA0AB05"]}]},{"name":"Ministry of Education of China","award":["2021FNA02008"],"award-info":[{"award-number":["2021FNA02008"]}]},{"name":"NSF-Fujian-China","award":["2022J01004"],"award-info":[{"award-number":["2022J01004"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,9,10]]},"DOI":"10.1145\/3603269.3604843","type":"proceedings-article","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T16:16:29Z","timestamp":1693584989000},"page":"152-166","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Beyond a Centralized Verifier: Scaling Data Plane Checking via Distributed, On-Device Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-6279","authenticated-orcid":false,"given":"Qiao","family":"Xiang","sequence":"first","affiliation":[{"name":"Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4368-9701","authenticated-orcid":false,"given":"Chenyang","family":"Huang","sequence":"additional","affiliation":[{"name":"Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8851-9725","authenticated-orcid":false,"given":"Ridi","family":"Wen","sequence":"additional","affiliation":[{"name":"Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7980-0689","authenticated-orcid":false,"given":"Yuxin","family":"Wang","sequence":"additional","affiliation":[{"name":"Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5546-1774","authenticated-orcid":false,"given":"Xiwen","family":"Fan","sequence":"additional","affiliation":[{"name":"Xiamen University, Xiamen, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9119-1679","authenticated-orcid":false,"given":"Zaoxing","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, MD, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9266-3044","authenticated-orcid":false,"given":"Linghe","family":"Kong","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6304-9448","authenticated-orcid":false,"given":"Dennis","family":"Duan","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0372-5045","authenticated-orcid":false,"given":"Franck","family":"Le","sequence":"additional","affiliation":[{"name":"IBM Research, Yorktown Heights, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4273-9737","authenticated-orcid":false,"given":"Wei","family":"Sun","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tiramisu: Fast Multilayer Network Verification. In NSDI'20","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In NSDI'20. USENIX, 201--219."},{"key":"e_1_3_2_1_2_1","volume-title":"Commodity Data Center Network Architecture. In SIGCOMM'08","author":"Al-Fares Mohammad","year":"2008","unstructured":"Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. 2008. A Scalable, Commodity Data Center Network Architecture. In SIGCOMM'08. ACM, 63--74."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Ehab Al-Shaer and Saeed Al-Haj. 2010. FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In SafeConfig'10. ACM 37--44.","DOI":"10.1145\/1866898.1866905"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_1_6_1","unstructured":"Barefoot. 2019. UfiSpace S9180-32X S9180-32X Switch. https:\/\/www.ufispace.com\/uploads\/able\/files\/productfilemanager\/000045467d1fc648d792c404372956a0.pdf."},{"key":"e_1_3_2_1_7_1","volume-title":"Katra: Realtime Verification for Multilayer Networks. In NSDI'22","author":"Beckett Ryan","year":"2022","unstructured":"Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. In NSDI'22. USENIX, 617--634."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_9_1","volume-title":"Control Plane Compression. In SIGCOMM'18","author":"Beckett Ryan","year":"2018","unstructured":"Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2018. Control Plane Compression. In SIGCOMM'18. ACM, 476--489."},{"key":"e_1_3_2_1_10_1","volume-title":"Abstract Interpretation of Distributed Network Control Planes. PACMPL'19","author":"Beckett Ryan","year":"2019","unstructured":"Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2019. Abstract Interpretation of Distributed Network Control Planes. PACMPL'19, 1--27."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_3_2_1_12_1","volume-title":"Ddnf: An Efficient Data Structure for Header Spaces. In HVC'16","author":"Bj\u00f8rner Nikolaj","year":"2016","unstructured":"Nikolaj Bj\u00f8rner, Garvit Juniwal, Ratul Mahajan, Sanjit A Seshia, and George Varghese. 2016. Ddnf: An Efficient Data Structure for Header Spaces. In HVC'16. Springer, 49--64."},{"key":"e_1_3_2_1_13_1","volume-title":"SIGCOMM'14","author":"Bosshart Pat","year":"2014","unstructured":"Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, et al. 2014. P4: Programming Protocol-Independent Packet Processors. In SIGCOMM'14. ACM, 87--95."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_15_1","volume-title":"Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods. In MASSW'19","author":"Chen Shenghui","year":"2019","unstructured":"Shenghui Chen, Zhiming Fan, Haiying Shen, and Lu Feng. 2019. Performance Modeling and Verification of Load Balancing in Cloud Systems Using Formal Methods. In MASSW'19. IEEE, 146--151."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230546"},{"key":"e_1_3_2_1_17_1","volume-title":"Inferring Persistent Interdomain Congestion. In SIGCOMM'18","author":"Dhamdhere Amogh","year":"2018","unstructured":"Amogh Dhamdhere, David D Clark, Alexander Gamero-Garrido, Matthew Luckie, Ricky KP Mok, Gautam Akiwate, Kabir Gogia, Vaibhav Bajpai, Alex C Snoeren, and Kc Claffy. 2018. Inferring Persistent Interdomain Congestion. In SIGCOMM'18. ACM, 1--15."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405888"},{"key":"e_1_3_2_1_19_1","unstructured":"Edgecore. 2021. Edgecore Wedge32-100X Switch. https:\/\/www.edge-core.com\/productsInfo.php?cls=1&cls2=5&cls3=181&id=335."},{"key":"e_1_3_2_1_20_1","volume-title":"NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In NSDI'18","author":"El-Hassany Ahmed","year":"2018","unstructured":"Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2018. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In NSDI'18. USENIX, 579--594."},{"key":"e_1_3_2_1_21_1","volume-title":"OSDI'16","author":"Fayaz Seyed K","year":"2016","unstructured":"Seyed K Fayaz, Tushar Sharma, Ari Fogel, Ratul Mahajan, Todd Millstein, Vyas Sekar, and George Varghese. 2016. Efficient Network Reachability Analysis Using a Succinct Control Plane Representation. In OSDI'16. USENIX, 217--232."},{"key":"e_1_3_2_1_22_1","unstructured":"fb 10-2021. 2021. Facebook Employees Were Unable to Access Critical Work Tools During Six-Hour Outage. https:\/\/www.cnbc.com\/2021\/10\/04\/facebook-workers-lose-access-to-internal-tools-following-outage.html."},{"key":"e_1_3_2_1_23_1","volume-title":"Detecting BGP Configuration Faults with Static Analysis. In NSDI'05","author":"Feamster Nick","year":"2005","unstructured":"Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In NSDI'05. USENIX, 43--56."},{"key":"e_1_3_2_1_24_1","volume-title":"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 NSDI'15. USENIX, 469--483."},{"key":"e_1_3_2_1_25_1","unstructured":"Open Networking Foundation. 2015. Open Networking Foundation. https:\/\/www.opennetworking.org\/images\/stories\/downloads\/sdn-resources\/onf-specifications\/openflow\/openflow-spec-v1.5.1.pdf."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132753"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Aaron Gember-Jacobson Costin Raiciu and Laurent Vanbever. 2017. Integrating verification and repair into the control plane. In HotNets'17. ACM 129--135.","DOI":"10.1145\/3152434.3152439"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28094993"},{"key":"e_1_3_2_1_30_1","unstructured":"Google. 2020. A Language-Neutral Platform-Neutral Extensible Mechanism for Serializing Structured Data. urlhttps:\/\/developers.google.com\/protocol-buffers."},{"key":"e_1_3_2_1_31_1","unstructured":"Facebook Group. 2016. Facebook Open\/R. https:\/\/github.com\/facebook\/openr."},{"key":"e_1_3_2_1_32_1","unstructured":"Network Working Group. 1998. OSPF Version 2. https:\/\/www.rfc-editor.org\/rfc\/rfc2328.html."},{"key":"e_1_3_2_1_33_1","unstructured":"Dong Guo. 2022. Flash Artifact for SIGCOMM22. https:\/\/github.com\/snlab\/flash."},{"key":"e_1_3_2_1_34_1","volume-title":"Consistent Data Plane Verification for Large-Scale Network Settings. In SIGCOMM'22","author":"Guo Dong","unstructured":"Dong Guo, Shenshen Chen, Kai Gao, Qiao Xiang, Ying Zhang, and Y. Richard Yang. 2022. Flash: Fast, Consistent Data Plane Verification for Large-Scale Network Settings. In SIGCOMM'22 (Amsterdam, Netherlands). ACM, 314--335."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230545"},{"key":"e_1_3_2_1_36_1","volume-title":"Theory of machines and computations","author":"Hopcroft John","unstructured":"John Hopcroft. 1971. An n log n algorithm for minimizing states in a finite automaton. In Theory of machines and computations. Elsevier, 189--196."},{"key":"e_1_3_2_1_37_1","volume-title":"Delta-Net: Real-Time Network Verification Using Atoms. In NSDI'17","author":"Horn Alex","year":"2017","unstructured":"Alex Horn, Ali Kheradmand, and Mukul Prasad. 2017. Delta-Net: Real-Time Network Verification Using Atoms. In NSDI'17. USENIX, 735--749."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2019.8888144"},{"key":"e_1_3_2_1_39_1","volume-title":"Contra: A Programmable System for Performance-Aware Routing. In NSDI'20","author":"Hsu Kuo-Feng","year":"2020","unstructured":"Kuo-Feng Hsu, Ryan Beckett, Ang Chen, Jennifer Rexford, Praveen Tammana, and David Walker. 2020. Contra: A Programmable System for Performance-Aware Routing. In NSDI'20. USENIX, 701--721."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486019"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_42_1","volume-title":"GRooT: Proactive Verification of DNS Configurations. In SIGCOMM'20","author":"Reddy Kakarla Siva Kesava","year":"2020","unstructured":"Siva Kesava Reddy Kakarla, Ryan Beckett, Behnaz Arzani, Todd Millstein, and George Varghese. 2020. GRooT: Proactive Verification of DNS Configurations. In SIGCOMM'20. ACM, 310--328."},{"key":"e_1_3_2_1_43_1","volume-title":"NSDI'13","author":"Kazemian Peyman","year":"2013","unstructured":"Peyman Kazemian, Michael Chan, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis.. In NSDI'13. USENIX, 99--111."},{"key":"e_1_3_2_1_44_1","volume-title":"NSDI'12","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks.. In NSDI'12. USENIX, 113--126."},{"key":"e_1_3_2_1_45_1","volume-title":"Veriflow: Verifying Network-Wide Invariants in Real Time. In NSDI'13","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2013. Veriflow: Verifying Network-Wide Invariants in Real Time. In NSDI'13. USENIX, 15--27."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2012.121112.00190"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1282380.1282408"},{"key":"e_1_3_2_1_49_1","volume-title":"Theory and New Primitives for Safely Connecting Routing Protocol Instances. In SIGCOMM'10","author":"Le Franck","year":"2010","unstructured":"Franck Le, Geoffrey G Xie, and Hui Zhang. 2010. Theory and New Primitives for Safely Connecting Routing Protocol Instances. In SIGCOMM'10. ACM, 219--230."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/300307.1040360"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_53_1","volume-title":"Checking Beliefs in Dynamic Networks. In NSDI'15","author":"Lopes Nuno P","year":"2015","unstructured":"Nuno P Lopes, Nikolaj Bj\u00f8rner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In NSDI'15. USENIX, 499--512."},{"key":"e_1_3_2_1_54_1","volume-title":"Fast BGP Simulation of Large Datacenters. In VMCAI'19","author":"Lopes Nuno P","year":"2019","unstructured":"Nuno P Lopes and Andrey Rybalchenko. 2019. Fast BGP Simulation of Large Datacenters. In VMCAI'19. Springer, 386--408."},{"key":"e_1_3_2_1_55_1","volume-title":"Debugging the Data Plane with Anteater. SIGCOMM'11","author":"Mai Haohui","year":"2011","unstructured":"Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. SIGCOMM'11, 290--301."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"crossref","unstructured":"Gary S. Malkin. 1998. RIP Version 2. https:\/\/rfc-editor.org\/rfc\/rfc2453.txt.","DOI":"10.17487\/rfc2453"},{"key":"e_1_3_2_1_57_1","unstructured":"Mellanox. 2015. Mellanox SN2700 Switch. https:\/\/www.mellanox.com\/related-docs\/prod_eth_switches\/PB_SN2700.pdf."},{"key":"e_1_3_2_1_58_1","unstructured":"Microsoft. 2021. SONiC: The Networking Switch Software That Powers the Microsoft Global Cloud. https:\/\/azure.github.io\/SONiC\/."},{"key":"e_1_3_2_1_59_1","unstructured":"The Internet2 Observatory. 2021. The Internet2 Dataset. http:\/\/www.internet2.edu\/research-solutions\/research-support\/observatory."},{"key":"e_1_3_2_1_60_1","volume-title":"Verifying Reachability in Networks with Mutable Datapaths. In NSDI'17","author":"Panda Aurojit","year":"2017","unstructured":"Aurojit Panda, Ori Lahav, Katerina Argyraki, Mooly Sagiv, and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths. In NSDI'17. USENIX, 699--718."},{"key":"e_1_3_2_1_61_1","volume-title":"Scaling Network Verification Using Symmetry and Surgery. In SIGPLAN'16","author":"Plotkin Gordon D","year":"2016","unstructured":"Gordon D Plotkin, Nikolaj Bj\u00f8rner, Nuno P Lopes, Andrey Rybalchenko, and George Varghese. 2016. Scaling Network Verification Using Symmetry and Surgery. In SIGPLAN'16. ACM, 69--83."},{"key":"e_1_3_2_1_62_1","volume-title":"Plankton: Scalable Network Configuration Verification Through Model Checking. In NSDI'20","author":"Prabhu Santhosh","year":"2020","unstructured":"Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable Network Configuration Verification Through Model Checking. In NSDI'20. USENIX, 953--967."},{"key":"e_1_3_2_1_63_1","unstructured":"Open Compute Project. 2021. Open Network Linux. http:\/\/opennetlinux.org\/."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Yakov Rekhter Susan Hares and Dr. Tony Li. 2006. A Border Gateway Protocol 4 (BGP-4). https:\/\/rfc-editor.org\/rfc\/rfc4271.txt.","DOI":"10.17487\/rfc4271"},{"key":"e_1_3_2_1_65_1","unstructured":"sonic 10-2021. 2022. SONiC High Level Design. https:\/\/github.com\/sonic-net\/SONiC\/pull\/948."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2018.2867239"},{"key":"e_1_3_2_1_67_1","volume-title":"Measuring ISP Topologies with Rocketfuel. In SIGCOMM'02","author":"Spring Neil","year":"2002","unstructured":"Neil Spring, Ratul Mahajan, and David Wetherall. 2002. Measuring ISP Topologies with Rocketfuel. In SIGCOMM'02. ACM, 133--145."},{"key":"e_1_3_2_1_68_1","volume-title":"Probabilistic Verification of Network Configurations. In SIGCOMM'20","author":"Steffen Samuel","year":"2020","unstructured":"Samuel Steffen, Timon Gehr, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2020. Probabilistic Verification of Network Configurations. In SIGCOMM'20. ACM, 750--764."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3482898.3483360"},{"key":"e_1_3_2_1_70_1","volume-title":"Safely and Automatically Updating In-Network ACL Configurations with Intent Language. In SIGCOMM'19","author":"Tian Bingchuan","year":"2019","unstructured":"Bingchuan Tian, Xinyi Zhang, Ennan Zhai, Hongqiang Harry Liu, Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, et al. 2019. Safely and Automatically Updating In-Network ACL Configurations with Intent Language. In SIGCOMM'19. ACM, 214--226."},{"key":"e_1_3_2_1_71_1","unstructured":"A. Vahidi. 2020. A BDD and Z-BDD Library Written in Java. https:\/\/bitbucket.org\/vahidi\/jdd."},{"key":"e_1_3_2_1_72_1","volume-title":"On the Co-Existence of Distributed and Centralized Routing Control-Planes. In INFOCOM'15","author":"Vissicchio Stefano","year":"2015","unstructured":"Stefano Vissicchio, Luca Cittadini, Olivier Bonaventure, Geoffrey G Xie, and Laurent Vanbever. 2015. On the Co-Existence of Distributed and Centralized Routing Control-Planes. In INFOCOM'15. IEEE, 469--477."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2012.2187924"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"crossref","unstructured":"HuazheWang Chen Qian Ye Yu Hongkun Yang and Simon S Lam. 2015. Practical Network-Wide Packet Behavior Identification by AP Classifier. In CoNEXT'15. ACM 1--13.","DOI":"10.1145\/2716281.2836095"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720637"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_77_1","unstructured":"WonderNetwork. 2021. Global Ping Statistics. https:\/\/wondernetwork.com\/pings."},{"key":"e_1_3_2_1_78_1","volume-title":"Xiamen University","author":"SNGroup","year":"2022","unstructured":"SNGroup, Xiamen University. 2022. Tulkun Demos. http:\/\/distributeddpvdemo.tech\/."},{"key":"e_1_3_2_1_79_1","volume-title":"Xiamen University","author":"SNGroup","year":"2023","unstructured":"SNGroup, Xiamen University. 2023. Tulkun Prototype. https:\/\/github.com\/sngroup-xmu\/ddpv-pubilc.git."},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"crossref","unstructured":"Qiao Xiang Ridi Wen Chenyang Huang Yuxin Wang and Franck Le. 2022. Network can check itself: scaling data plane checking via distributed on-device verification. In HotNets'22. ACM 85--92.","DOI":"10.1145\/3563766.3564095"},{"key":"e_1_3_2_1_82_1","volume-title":"On Static Reachability Analysis of IP Networks. In INFOCOM'05","author":"Xie Geoffrey G","year":"2005","unstructured":"Geoffrey G Xie, Jibin Zhan, David A Maltz, Hui Zhang, Albert Greenberg, Gisli Hjalmtysson, and Jennifer Rexford. 2005. On Static Reachability Analysis of IP Networks. In INFOCOM'05. IEEE, 2170--2183."},{"key":"e_1_3_2_1_83_1","volume-title":"Real-Time Verification of Network Properties Using Atomic Predicates. In ICNP'13","author":"Yang Hongkun","year":"2013","unstructured":"Hongkun Yang and Simon S Lam. 2013. Real-Time Verification of Network Properties Using Atomic Predicates. In ICNP'13. IEEE, 1--11."},{"key":"e_1_3_2_1_84_1","volume-title":"Collaborative Verification of Forward and Reverse Reachability in the Internet Data Plane. In ICNP'14","author":"Yang Hongkun","year":"2014","unstructured":"Hongkun Yang and Simon S Lam. 2014. Collaborative Verification of Forward and Reverse Reachability in the Internet Data Plane. In ICNP'14. IEEE, 320--331."},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3406217"},{"key":"e_1_3_2_1_88_1","volume-title":"NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification. In NSDI'20","author":"Yuan Yifei","year":"2020","unstructured":"Yifei Yuan, Soo-Jin Moon, Sahil Uppal, Limin Jia, and Vyas Sekar. 2020. NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification. In NSDI'20. USENIX, 181--200."},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_1_90_1","volume-title":"Libra: Divide and Conquer To Verify Forwarding Tables in Huge Networks. In 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 NSDI'14. USENIX, 87--99."},{"key":"e_1_3_2_1_91_1","volume-title":"Automated Verification of Customizable Middlebox Properties with Gravel. In NSDI'20","author":"Zhang Kaiyuan","year":"2020","unstructured":"Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang. 2020. Automated Verification of Customizable Middlebox Properties with Gravel. In NSDI'20. USENIX, 221--239."},{"key":"e_1_3_2_1_92_1","volume-title":"Differential Network Analysis. In NSDI'22","author":"Zhang Peng","year":"2022","unstructured":"Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. 2022. Differential Network Analysis. In NSDI'22. USENIX, 601--615."},{"key":"e_1_3_2_1_93_1","volume-title":"APKeep: Realtime Verification for Real Networks. In NSDI'20","author":"Zhang Peng","year":"2020","unstructured":"Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In NSDI'20. USENIX, 241--255."},{"key":"e_1_3_2_1_94_1","volume-title":"Private and Verifiable Interdomain Routing Decisions. In SIGCOMM'12","author":"Zhao Mingchen","year":"2012","unstructured":"Mingchen Zhao, Wenchao Zhou, Alexander JT Gurney, Andreas Haeberlen, Micah Sherr, and Boon Thau Loo. 2012. Private and Verifiable Interdomain Routing Decisions. In SIGCOMM'12. ACM, 383--394."},{"key":"e_1_3_2_1_95_1","volume-title":"ICNP'16","author":"Zheng Jiaqi","year":"2016","unstructured":"Jiaqi Zheng, Hong Xu, Xiaojun Zhu, Guihai Chen, and Yanhui Geng. 2016. We've got you covered: Failure recovery with backup tunnels in traffic engineering. In ICNP'16. IEEE, 1--10."}],"event":{"name":"ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference","location":"New York NY USA","acronym":"ACM SIGCOMM '23","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2023 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604843","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3603269.3604843","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:42Z","timestamp":1750178802000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":94,"alternative-id":["10.1145\/3603269.3604843","10.1145\/3603269"],"URL":"https:\/\/doi.org\/10.1145\/3603269.3604843","relation":{},"subject":[],"published":{"date-parts":[[2023,9]]},"assertion":[{"value":"2023-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}