{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T07:17:57Z","timestamp":1760426277880,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["2024PTB-004"],"award-info":[{"award-number":["2024PTB-004"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"China Postdoctoral Science Foundation","doi-asserted-by":"publisher","award":["BX20230052,2024M750256"],"award-info":[{"award-number":["BX20230052,2024M750256"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Natural Science Foundation of China under Grants","award":["62401080,62471055,62101064,U23B2001,62321001,62171057,62201072"],"award-info":[{"award-number":["62401080,62471055,62101064,U23B2001,62321001,62171057,62201072"]}]},{"DOI":"10.13039\/501100006374","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2024YFE0200800"],"award-info":[{"award-number":["2024YFE0200800"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ministry of Education and China Mobile Joint Fund","award":["MCM20200202,MCM20180101"],"award-info":[{"award-number":["MCM20200202,MCM20180101"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,30]]},"DOI":"10.1145\/3689031.3717494","type":"proceedings-article","created":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T06:25:20Z","timestamp":1742970320000},"page":"1350-1364","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Atlas: Towards Real-Time Verification in Large-Scale Networks via a Native Distributed Architecture"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4155-0605","authenticated-orcid":false,"given":"Mingxiao","family":"Ma","sequence":"first","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5666-6440","authenticated-orcid":false,"given":"Yuehan","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2182-2228","authenticated-orcid":false,"given":"Jingyu","family":"Wang","sequence":"additional","affiliation":[{"name":"Pengcheng Laboratory"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1301-4981","authenticated-orcid":false,"given":"Bo","family":"He","sequence":"additional","affiliation":[{"name":"E-Byte.com"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2550-756X","authenticated-orcid":false,"given":"Chenyang","family":"Zhao","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0829-4624","authenticated-orcid":false,"given":"Qi","family":"Qi","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3345-1732","authenticated-orcid":false,"given":"Zirui","family":"Zhuang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3072-7422","authenticated-orcid":false,"given":"Haifeng","family":"Sun","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6999-6262","authenticated-orcid":false,"given":"Lingqi","family":"Guo","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9497-6802","authenticated-orcid":false,"given":"Yuebin","family":"Guo","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-7050","authenticated-orcid":false,"given":"Gong","family":"Zhang","sequence":"additional","affiliation":[{"name":"Huawei Technologies"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1486-0573","authenticated-orcid":false,"given":"Jianxin","family":"Liao","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Delta-net dataset. https:\/\/github.com\/delta-net\/datasets."},{"key":"e_1_3_2_1_2_1","unstructured":"Libra dataset. https:\/\/github.com\/jvimal\/libra-data."},{"key":"e_1_3_2_1_3_1","unstructured":"Topozoo overview. http:\/\/www.topology-zoo.org\/dataset.html."},{"key":"e_1_3_2_1_4_1","unstructured":"Vahidi A. Jdd. https:\/\/bitbucket.org\/vahidi\/jdd."},{"key":"e_1_3_2_1_5_1","volume-title":"Tiramisu: Fast and general network verification. arXiv preprint arXiv:1906.02043","author":"Abhashkumar Anubhavnidhi","year":"2019","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast and general network verification. arXiv preprint arXiv:1906.02043, 2019."},{"key":"e_1_3_2_1_6_1","volume-title":"A scalable, commodity data center network architecture. ACM SIGCOMM computer communication review, 38(4):63--74","author":"Al-Fares Mohammad","year":"2008","unstructured":"Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. A scalable, commodity data center network architecture. ACM SIGCOMM computer communication review, 38(4):63--74, 2008."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866898.1866905"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"e_1_3_2_1_9_1","volume-title":"Introducing data center fabric, the next-generation facebook data center network","author":"Andreyev Alexey","year":"2014","unstructured":"Alexey Andreyev. Introducing data center fabric, the next-generation facebook data center network, 2014. https:\/\/engineering.fb.com\/2014\/11\/14\/production-engineering\/introducing-data-center-fabric-the-next-generation-facebook-data-center-network\/."},{"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","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_4"},{"key":"e_1_3_2_1_12_1","volume-title":"Website","author":"Donnelly Caroline","year":"2023","unstructured":"Caroline Donnelly. Microsoft 365 outage affecting teams, outlook and azure users blamed on 'networking fault'. Website, 2023. https:\/\/www.computerweekly.com\/news\/252529561\/Microsoft-365-outage-affecting-Teams-Outlook-and-Azure-users-blamed-on-networking-fault."},{"key":"e_1_3_2_1_13_1","first-page":"217","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (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. Efficient network reachability analysis using a succinct control plane representation. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 217--232, 2016."},{"key":"e_1_3_2_1_14_1","first-page":"469","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. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 469--483, 2015."},{"key":"e_1_3_2_1_15_1","unstructured":"Google. Protobuf overview. https:\/\/protobuf.dev\/."},{"key":"e_1_3_2_1_16_1","volume-title":"Mar","author":"Greenberg Albert","year":"2011","unstructured":"Albert Greenberg, James R. Hamilton, Navendu Jain, Srikanth Kandula, Changhoon Kim, Parantap Lahiri, David A. Maltz, Parveen Patel, and Sudipta Sengupta. Vl2. Communications of the ACM, page 95--104, Mar 2011."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544246"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3610845"},{"key":"e_1_3_2_1_19_1","volume-title":"Google suffers global outage with gmail, youtube and majority of services affected. The Guardian (Dec","author":"Hern Alex","year":"2020","unstructured":"Alex Hern. Google suffers global outage with gmail, youtube and majority of services affected. The Guardian (Dec. 2020). https:\/\/www.the-guardian. com\/technology\/2020\/dec\/14\/google-suffers-worldwide-outage-with-gmail-youtube-and-other-services-down, 2020."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230545"},{"key":"e_1_3_2_1_21_1","first-page":"735","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Horn Alex","year":"2017","unstructured":"Alex Horn, Ali Kheradmand, and Mukul Prasad. Delta-net: Real-time network verification using atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17), pages 735--749, 2017."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2019.8888144"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_24_1","volume-title":"Networked Systems Design and Implementation","author":"Kazemian Peyman","year":"2013","unstructured":"Peyman Kazemian, MichaelT. Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. Real time network policy checking using header space analysis. Networked Systems Design and Implementation, Networked Systems Design and Implementation, Apr 2013."},{"key":"e_1_3_2_1_25_1","first-page":"113","volume-title":"9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12)","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 113--126, 2012."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229584.3229585"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"e_1_3_2_1_29_1","unstructured":"Will Paul. Wondernetwork 2021. https:\/\/wondernetwork.com\/pings.\/."},{"key":"e_1_3_2_1_30_1","first-page":"1","volume-title":"Disco: Distributed multi-domain sdn controllers. In 2014 IEEE network operations and management symposium (NOMS)","author":"Phemius Kevin","year":"2014","unstructured":"Kevin Phemius, Mathieu Bouet, and J\u00e9r\u00e9mie Leguay. Disco: Distributed multi-domain sdn controllers. In 2014 IEEE network operations and management symposium (NOMS), pages 1--4. IEEE, 2014."},{"key":"e_1_3_2_1_31_1","first-page":"953","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Prabhu Santhosh","year":"2020","unstructured":"Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. Plankton: Scalable network configuration verification through model checking. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 953--967, 2020."},{"volume-title":"ddpv-pubilc","year":"2023","key":"e_1_3_2_1_32_1","unstructured":"sngroup xmu. ddpv-pubilc, 2023. https:\/\/github.com\/sngroup-xmu\/ddpv-pubilc."},{"volume-title":"Flash artifact for sigcomm22","year":"2022","key":"e_1_3_2_1_33_1","unstructured":"snlab. Flash artifact for sigcomm22, 2022. https:\/\/github.com\/snlab\/flash."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3663408.3663420"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2017.03.004"},{"key":"e_1_3_2_1_37_1","unstructured":"Wikipedia. Bdd overview. https:\/\/en.wikipedia.org\/wiki\/Binary_decisiondiagram."},{"key":"e_1_3_2_1_38_1","unstructured":"Wikipedia. Clos network. https:\/\/en.wikipedia.org\/wiki\/Clos_network."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604843"},{"key":"e_1_3_2_1_40_1","first-page":"887","volume-title":"Real-time verification of network properties using atomic predicates","author":"Yang Hongkun","year":"2016","unstructured":"Hongkun Yang and Simon S. Lam. Real-time verification of network properties using atomic predicates. IEEE\/ACM Transactions on Networking, page 887--900, Apr 2016."},{"key":"e_1_3_2_1_41_1","first-page":"601","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Zhang Peng","year":"2022","unstructured":"Peng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang, Xu Liu, and Hao Li. Differential network analysis. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22), pages 601--615, 2022."},{"key":"e_1_3_2_1_42_1","first-page":"241","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","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 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 241--255, 2020."},{"key":"e_1_3_2_1_43_1","volume-title":"21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Zhao Chenyang","year":"2024","unstructured":"Chenyang Zhao, Yuebin Guo, Jingyu Wang, Qi Qi, Zirui Zhuang, Haifeng Sun, Lingqi Guo, Yuming Xie, and Jianxin Liao. EPVerifier: Accelerating update storms verification with Edge-Predicate. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24), Santa Clara, CA, April 2024. USENIX Association."}],"event":{"name":"EuroSys '25: Twentieth European Conference on Computer Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Rotterdam Netherlands","acronym":"EuroSys '25"},"container-title":["Proceedings of the Twentieth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3717494","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689031.3717494","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T11:18:08Z","timestamp":1755775088000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3717494"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":43,"alternative-id":["10.1145\/3689031.3717494","10.1145\/3689031"],"URL":"https:\/\/doi.org\/10.1145\/3689031.3717494","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}