{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T23:19:15Z","timestamp":1769555955440,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","funder":[{"name":"National Key Research and Development Program of China","award":["2022YFB2901403"],"award-info":[{"award-number":["2022YFB2901403"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62272382"],"award-info":[{"award-number":["62272382"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62172323"],"award-info":[{"award-number":["62172323"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,8]]},"DOI":"10.1145\/3718958.3750516","type":"proceedings-article","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T16:54:11Z","timestamp":1756313651000},"page":"796-808","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["S2: A Distributed Configuration Verifier for Hyper-Scale Networks"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-4078-7616","authenticated-orcid":false,"given":"Dan","family":"Wang","sequence":"first","affiliation":[{"name":"Xi'an Jiaotong University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7721-2675","authenticated-orcid":false,"given":"Peng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenbing","family":"Sun","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1756-9162","authenticated-orcid":false,"given":"Wenkai","family":"Li","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xing","family":"Feng","sequence":"additional","affiliation":[{"name":"NorthWest University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8776-6911","authenticated-orcid":false,"given":"Hao","family":"Li","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9491-2524","authenticated-orcid":false,"given":"Jiawei","family":"Chen","sequence":"additional","affiliation":[{"name":"ByteDance"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weirong","family":"Jiang","sequence":"additional","affiliation":[{"name":"ByteDance"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongping","family":"Tang","sequence":"additional","affiliation":[{"name":"ByteDance"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,8,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Configure and Verify the BGP Conditional Advertisement Feature. https:\/\/www.cisco.com\/c\/en\/us\/support\/docs\/ip\/border-gateway-protocol-bgp\/16137-cond-adv.html."},{"key":"e_1_3_2_1_2_1","unstructured":"Graphical network simulator-3 (GNS3). https:\/\/gns3.com."},{"key":"e_1_3_2_1_3_1","unstructured":"Metis. http:\/\/glaros.dtc.umn.edu\/gkhome\/views\/metis."},{"key":"e_1_3_2_1_4_1","unstructured":"Protocol Buffers (ProtoBuf). https:\/\/protobuf.dev\/."},{"key":"e_1_3_2_1_5_1","volume-title":"USENIX NSDI","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast and general network verification. In USENIX NSDI, 2020."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the ACM on Programming Languages, 7(PLDI):50\u201375","author":"Thijm Timothy Alberdingk","year":"2023","unstructured":"Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Modular control plane verification via temporal invariants. Proceedings of the ACM on Programming Languages, 7(PLDI):50\u201375, 2023."},{"key":"e_1_3_2_1_7_1","first-page":"124","volume-title":"Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures","author":"Andreev Konstantin","year":"2004","unstructured":"Konstantin Andreev and Harald R\u00e4cke. Balanced graph partitioning. In Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures, pages 120\u2013124, 2004."},{"key":"e_1_3_2_1_8_1","first-page":"131","volume-title":"Proceedings of the Nineteenth European Conference on Computer Systems","author":"Bai Songyuan","year":"2024","unstructured":"Songyuan Bai, Hao Zheng, Chen Tian, Xiaoliang Wang, Chang Liu, Xin Jin, Fu Xiao, Qiao Xiang, Wanchun Dou, and Guihai Chen. Unison: A parallel-efficient and user-transparent network simulation kernel. In Proceedings of the Nineteenth European Conference on Computer Systems, pages 115\u2013131, 2024."},{"key":"e_1_3_2_1_9_1","first-page":"634","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Beckett Ryan","year":"2022","unstructured":"Ryan Beckett and Aarti Gupta. Katra: Realtime verification for multilayer networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pages 617\u2013634, 2022."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_11_1","volume-title":"ACM SIGCOMM","author":"Beckett Ryan","year":"2018","unstructured":"Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Control plane compression. In ACM SIGCOMM, 2018."},{"key":"e_1_3_2_1_12_1","volume-title":"ACM POPL","author":"Beckett Ryan","year":"2020","unstructured":"Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract interpretation of distributed network control planes. In ACM POPL, 2020."},{"key":"e_1_3_2_1_13_1","volume-title":"ACM SIGCOMM","author":"Beckett Ryan","year":"2016","unstructured":"Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. Don't mind the gap: Bridging network-wide objectives and device-level configurations. In ACM SIGCOMM, 2016."},{"key":"e_1_3_2_1_14_1","first-page":"135","volume-title":"Proceedings of the ACM SIGCOMM 2023 Conference","author":"Brown Matt","year":"2023","unstructured":"Matt Brown, Ari Fogel, Daniel Halperin, Victor Heorhiadi, Ratul Mahajan, and Todd Millstein. Lessons from the evolution of the batfish configuration analysis tool. In Proceedings of the ACM SIGCOMM 2023 Conference, pages 122\u2013135, 2023."},{"key":"e_1_3_2_1_15_1","first-page":"356","volume-title":"Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication","author":"Choi Sean","year":"2018","unstructured":"Sean Choi, Boris Burkov, Alex Eckert, Tian Fang, Saman Kazemkhani, Rob Sherwood, Ying Zhang, and Hongyi Zeng. Fboss: building switch software at scale. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 342\u2013356, 2018."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1953.tb01433.x"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_3_2_1_18_1","unstructured":"Ari Fogel. Batfish. https:\/\/github.com\/batfish\/batfish."},{"key":"e_1_3_2_1_19_1","volume-title":"USENIX NSDI","author":"Fogel Ari","year":"2015","unstructured":"Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A general approach to network configuration analysis. In USENIX NSDI, 2015."},{"key":"e_1_3_2_1_20_1","first-page":"181","volume-title":"Proceedings of the ACM SIGCOMM 2023 Conference","author":"Gao Kaihui","year":"2023","unstructured":"Kaihui Gao, Li Chen, Dan Li, Vincent Liu, Xizheng Wang, Ran Zhang, and Lu Lu. Dons: Fast and affordable discrete event network simulation with automatic parallelization. In Proceedings of the ACM SIGCOMM 2023 Conference, pages 167\u2013181, 2023."},{"key":"e_1_3_2_1_21_1","volume-title":"21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Gao Zhaoyu","year":"2024","unstructured":"Zhaoyu Gao, Anubhavnidhi Abhashkumar, Zhen Sun, Weirong Jiang, and Yi Wang. Crescent: Emulating heterogeneous production network at scale. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24), Santa Clara, CA, April 2024. USENIX Association."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386019"},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. ACM Program. Lang., 5(ICFP)","author":"Giannarakis Nick","year":"2021","unstructured":"Nick Giannarakis, Alexandra Silva, and David Walker. Probnv: probabilistic verification of network control planes. Proc. ACM Program. Lang., 5(ICFP), 2021."},{"key":"e_1_3_2_1_25_1","unstructured":"Google. gRPC. https:\/\/grpc.io\/."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934891"},{"key":"e_1_3_2_1_27_1","first-page":"264","volume-title":"Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies, CoNEXT '12","author":"Handigol Nikhil","year":"2012","unstructured":"Nikhil Handigol, Brandon Heller, Vimalkumar Jeyakumar, Bob Lantz, and Nick McKeown. Reproducible network experiments using container-based emulation. In Proceedings of the 8th International Conference on Emerging Networking Experiments and Technologies, CoNEXT '12, page 253\u2013264, New York, NY, USA, 2012. Association for Computing Machinery."},{"key":"e_1_3_2_1_28_1","volume-title":"USENIX NSDI","author":"Horn Alex","year":"2017","unstructured":"Alex Horn, Ali Kheradmand, and Mukul R Prasad. Delta-net: Real-time network verification using atoms. In USENIX NSDI, 2017."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-71760-9"},{"key":"e_1_3_2_1_30_1","volume-title":"USENIX NSDI","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In USENIX NSDI, 2012."},{"key":"e_1_3_2_1_31_1","volume-title":"USENIX NSDI","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P Godfrey. VeriFlow: Verifying network-wide invariants in real time. In USENIX NSDI, 2013."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the ACM on Networking, 1(CoNEXT3):1\u2013 22","author":"Liu Xu","year":"2023","unstructured":"Xu Liu, Peng Zhang, Hao Li, and Wenbing Sun. Modular data plane verification for compositional networks. Proceedings of the ACM on Networking, 1(CoNEXT3):1\u2013 22, 2023."},{"key":"e_1_3_2_1_34_1","volume-title":"International Conference on Verification, Model Checking, and Abstract Interpretation","author":"Lopes Nuno P","year":"2019","unstructured":"Nuno P Lopes and Andrey Rybalchenko. Fast BGP simulation of large datacenters. In International Conference on Verification, Model Checking, and Abstract Interpretation, 2019."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2331515"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_37_1","volume-title":"ACM POPL","author":"Plotkin Gordon D","year":"2016","unstructured":"Gordon D Plotkin, Nikolaj Bj\u00f8rner, Nuno P Lopes, Andrey Rybalchenko, and George Varghese. Scaling network verification using symmetry and surgery. In ACM POPL, 2016."},{"key":"e_1_3_2_1_38_1","volume-title":"USENIX NSDI","author":"Prabhu Santhosh","year":"2020","unstructured":"Santhosh Prabhu, Kuan-Yen Chou, Ali Kheradmand, P Godfrey, and Matthew Caesar. Plankton: Scalable network configuration verification through model checking. In USENIX NSDI, 2020."},{"key":"e_1_3_2_1_39_1","unstructured":"Divya Raghunathan. Synthesized Fattrees. https:\/\/github.com\/divya-urs\/ACORN_benchmarks."},{"key":"e_1_3_2_1_40_1","first-page":"644","volume-title":"20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Ramanathan Sivaramakrishnan","year":"2023","unstructured":"Sivaramakrishnan Ramanathan, Ying Zhang, Mohab Gawish, Yogesh Mundada, Zhaodong Wang, Sangki Yun, Eric Lippert, Walid Taha, Minlan Yu, and Jelena Mirkovic. Practical intent-driven routing configuration synthesis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), pages 629\u2013644, 2023."},{"key":"e_1_3_2_1_41_1","volume-title":"Springer","author":"Riley George F","year":"2010","unstructured":"George F Riley and Thomas R Henderson. The ns-3 network simulator. In Modeling and tools for network simulation, pages 15\u201334. Springer, 2010."},{"key":"e_1_3_2_1_42_1","volume-title":"ACM SIGCOMM","author":"Steffen Samuel","year":"2020","unstructured":"Samuel Steffen, Timon Gehr, Petar Tsankov, Laurent Vanbever, and Martin Vechev. Probabilistic verification of network configurations. In ACM SIGCOMM, 2020."},{"key":"e_1_3_2_1_43_1","volume-title":"ACM SIGCOMM","author":"Eric Sung Yu-Wei","year":"2016","unstructured":"Yu-Wei Eric Sung, Xiaozheng Tie, Starsky H. Y. Wong, and Hongyi Zeng. Robotron: Top-down network management at facebook scale. In ACM SIGCOMM, 2016."},{"key":"e_1_3_2_1_44_1","volume-title":"Lightyear: Using modularity to scale bgp control plane verification. arXiv preprint arXiv:2204.09635","author":"Tang Alan","year":"2022","unstructured":"Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd Millstein, and George Varghese. Lightyear: Using modularity to scale bgp control plane verification. arXiv preprint arXiv:2204.09635, 2022."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2024.3360371"},{"key":"e_1_3_2_1_46_1","unstructured":"Arash Vahidi. JDD a pure Java BDD and Z-BDD library. https:\/\/bitbucket.org\/vahidi\/jdd\/."},{"key":"e_1_3_2_1_47_1","volume-title":"Springer","author":"Varga Andras","year":"2019","unstructured":"Andras Varga. A practical introduction to the omnet++ simulation framework. In Recent Advances in Network Simulation: The OMNeT++ Environment and its Ecosystem, pages 3\u201351. Springer, 2019."},{"key":"e_1_3_2_1_48_1","first-page":"212","volume-title":"Proceedings of the ACM SIGCOMM 2024 Conference","author":"Wang Dan","year":"2024","unstructured":"Dan Wang, Peng Zhang, and Aaron Gember-Jacobson. Expresso: Comprehensively reasoning about external routes using symbolic simulation. In Proceedings of the ACM SIGCOMM 2024 Conference, pages 197\u2013212, 2024."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_50_1","first-page":"166","volume-title":"Proceedings of the ACM SIGCOMM 2023 Conference","author":"Xiang Qiao","year":"2023","unstructured":"Qiao Xiang, Chenyang Huang, Ridi Wen, Yuxin Wang, Xiwen Fan, Zaoxing Liu, Linghe Kong, Dennis Duan, Franck Le, and Wei Sun. Beyond a centralized verifier: Scaling data plane checking via distributed, on-device verification. In Proceedings of the ACM SIGCOMM 2023 Conference, pages 152\u2013166, 2023."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2013.6733614"},{"key":"e_1_3_2_1_52_1","volume-title":"ACM SIGCOMM","author":"Ye Fangdan","year":"2020","unstructured":"Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, et al. Accuracy, scalability, coverage: A practical configuration verifier on a global WAN. In ACM SIGCOMM, 2020."},{"key":"e_1_3_2_1_53_1","first-page":"245","volume-title":"11th IEEE\/ACM International Symposium on Modeling, Analysis and Simulation of Computer Telecommunications Systems, 2003. MASCOTS 2003.","author":"Yocum Ken","unstructured":"Ken Yocum, Ethan Eade, Julius Degesys, David Becker, Jeff Chase, and Amin Vahdat. Toward scaling network emulation using topology partitioning. In 11th IEEE\/ACM International Symposium on Modeling, Analysis and Simulation of Computer Telecommunications Systems, 2003. MASCOTS 2003., pages 242\u2013245. IEEE, 2003."},{"key":"e_1_3_2_1_54_1","volume-title":"USENIX NSDI","author":"Zeng Hongyi","year":"2014","unstructured":"Hongyi Zeng, Shidong Zhang, Fei Ye, Vimalkumar Jeyakumar, Mickey Ju, Junda Liu, Nick McKeown, and Amin Vahdat. Libra: Divide and conquer to verify forwarding tables in huge networks. In USENIX NSDI, 2014."},{"key":"e_1_3_2_1_55_1","volume-title":"USENIX NSDI","author":"Zhang Peng","year":"2022","unstructured":"Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. Differential network analysis. In USENIX NSDI, 2022."},{"key":"e_1_3_2_1_56_1","volume-title":"USENIX NSDI","author":"Zhang Peng","year":"2020","unstructured":"Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. APKeep: Realtime verification for real networks. In USENIX NSDI, 2020."},{"key":"e_1_3_2_1_57_1","first-page":"349","volume-title":"Proceedings of the ACM SIGCOMM 2022 Conference, SIGCOMM '22","author":"Zhang Peng","year":"2022","unstructured":"Peng Zhang, Dan Wang, and Aaron Gember-Jacobson. Symbolic router execution. In Proceedings of the ACM SIGCOMM 2022 Conference, SIGCOMM '22, page 336\u2013349, New York, NY, USA, 2022. Association for Computing Machinery."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNSM.2023.3287030"}],"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.3750516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T16:57:19Z","timestamp":1756313839000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3718958.3750516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,27]]},"references-count":58,"alternative-id":["10.1145\/3718958.3750516","10.1145\/3718958"],"URL":"https:\/\/doi.org\/10.1145\/3718958.3750516","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"}}]}}