{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T02:32:01Z","timestamp":1782959521141,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":62,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,8,4]],"date-time":"2024-08-04T00:00:00Z","timestamp":1722729600000},"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":[[2024,8,4]]},"DOI":"10.1145\/3651890.3672246","type":"proceedings-article","created":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T13:11:43Z","timestamp":1722431503000},"page":"228-243","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A General and Efficient Approach to Verifying Traffic Load Properties under Arbitrary k Failures"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0607-0945","authenticated-orcid":false,"given":"Ruihan","family":"Li","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"},{"name":"Alibaba Cloud, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9089-580X","authenticated-orcid":false,"given":"Yifei","family":"Yuan","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Bellevue, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9031-2488","authenticated-orcid":false,"given":"Fangdan","family":"Ye","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7027-4566","authenticated-orcid":false,"given":"Mengqi","family":"Liu","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Bellevue, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2101-0173","authenticated-orcid":false,"given":"Ruizhen","family":"Yang","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7890-3561","authenticated-orcid":false,"given":"Yang","family":"Yu","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0316-6756","authenticated-orcid":false,"given":"Tianchen","family":"Guo","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5671-8431","authenticated-orcid":false,"given":"Qing","family":"Ma","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2015-189X","authenticated-orcid":false,"given":"Xianlong","family":"Zeng","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9171-2596","authenticated-orcid":false,"given":"Chenren","family":"Xu","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7272-8143","authenticated-orcid":false,"given":"Dennis","family":"Cai","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Sunnyvale, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4352-7497","authenticated-orcid":false,"given":"Ennan","family":"Zhai","sequence":"additional","affiliation":[{"name":"Alibaba Cloud, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"1981. Internet Protocol. RFC 791. (Sept. 1981). 10.17487\/RFC0791","DOI":"10.17487\/RFC0791"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1105"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1142"},{"key":"e_1_3_2_1_4_1","volume-title":"Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 201--219. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/abhashkumar"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1402958.1402967"},{"key":"e_1_3_2_1_6_1","volume-title":"Algebric decision diagrams and their applications. Formal methods in system design 10","author":"Bahar R Iris","year":"1997","unstructured":"R Iris Bahar, Erica A Frohm, Charles M Gaona, Gary D Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi. 1997. Algebric decision diagrams and their applications. Formal methods in system design 10 (1997), 171--206."},{"key":"e_1_3_2_1_7_1","volume-title":"Katra: Realtime Verification for Multilayer Networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Beckett Ryan","year":"2022","unstructured":"Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA, 617--634. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/beckett"},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342069"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604866"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3393691.3394195"},{"key":"e_1_3_2_1_14_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Chang Yiyang","year":"2017","unstructured":"Yiyang Chang, Sanjay Rao, and Mohit Tawarmalani. 2017. Robust Validation of Network Designs under Uncertain Demands and Failures. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 347--362. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/chang"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/157485.164569"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523715"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026895"},{"key":"e_1_3_2_1_18_1","unstructured":"Mikel Jimenez Fernandez and Henry Kwok. 2017. Building Express Backbone: Facebook's new long-haul network. (2017). https:\/\/en.wikipedia.org\/w\/index.php?title=Traffic_engineering_(transportation)&oldid=1169174329"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC8402"},{"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, Oakland, CA, 469--483. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/fogel"},{"key":"e_1_3_2_1_21_1","volume-title":"Probabilistic NetKAT","author":"Foster Nate","unstructured":"Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 282--309."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008647823331"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_24_1","volume-title":"Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement","author":"Giannarakis Nick","unstructured":"Nick Giannarakis, Ryan Beckett, Ratul Mahajan, and David Walker. 2019. Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 305--323."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386019"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473595"},{"key":"e_1_3_2_1_27_1","unstructured":"Peter L Hammer I Rosenberg Sergiu Rudeanu et al. 1963. On the determination of the minima of pseudo-Boolean functions. Studii si Cercetari matematice 14 (1963) 359--364."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486012"},{"key":"e_1_3_2_1_29_1","volume-title":"Delta-net: Real-time Network Verification Using Atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (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 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 735--749. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/horn-alex"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486019"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405871"},{"key":"e_1_3_2_1_34_1","volume-title":"Header Space Analysis: Static Checking for Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12)","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). USENIX Association, San Jose, CA, 113--126. https:\/\/www.usenix.org\/conference\/nsdi12\/technical-sessions\/presentation\/kazemian"},{"key":"e_1_3_2_1_35_1","first-page":"15","article-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). USENIX Association","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 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). USENIX Association, Lombard, IL, 15--27. https:\/\/www.usenix.org\/conference\/nsdi13\/technical-sessions\/presentation\/khurshid","journal-title":"Lombard"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_37_1","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Krishnaswamy Umesh","year":"2022","unstructured":"Umesh Krishnaswamy, Rachee Singh, Nikolaj Bj\u00f8rner, and Himanshu Raj. 2022. Decentralized cloud wide-area network traffic engineering with BLASTSHIELD. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22). USENIX Association, Renton, WA, 325--338. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/krishnaswamy"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787478"},{"key":"e_1_3_2_1_39_1","volume-title":"21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24)","author":"Li Ruihan","year":"2024","unstructured":"Ruihan Li, Fangdan Ye, Yifei Yuan, Ruizhen Yang, Bingchuan Tian, Tianchen Guo, Hao Wu, Xiaobo Zhu, Zhongyu Guan, Qing Ma, Xianlong Zeng, Chenren Xu, Dennis Cai, and Ennan Zhai. 2024. Reasoning about Network Traffic Load Property at Production Scale. In 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI 24). USENIX Association, Santa Clara, CA, 1063--1082. https:\/\/www.usenix.org\/conference\/nsdi24\/presentation\/li-ruihan"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626314"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Jed Liu William T. Hallahan Cole Schlesinger Milad Sharif Jeongkeun Lee Robert Soul\u00e9 Han Wang Calin Cascaval Nick McKeown and Nate Foster. 2018. p4v: Practical verification for programmable data planes. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_43_1","volume-title":"Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (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 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association, Oakland, CA, 499--512. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/lopes"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.209"},{"key":"e_1_3_2_1_46_1","volume-title":"Verifying Reachability in Networks with Mutable Datapaths. In 14th USENIX Symposium on Networked Systems Design and Implementation (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 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 699--718. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/panda-mutable-datapaths"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2005.1541716"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604834"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009843"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405900"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385976"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472937"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342088"},{"key":"e_1_3_2_1_55_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.)","author":"Velner Yaron","unstructured":"Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, and Sharon Shoham. 2016. Some Complexity Results for Stateful Network Verification. In Tools and Algorithms for the Construction and Analysis of Systems, Marsha Chechik and Jean-Fran\u00e7ois Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 811--830."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2012.2187924"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3406217"},{"key":"e_1_3_2_1_58_1","volume-title":"NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (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 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 181--200. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/yuan"},{"key":"e_1_3_2_1_59_1","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Zhai Ennan","year":"2020","unstructured":"Ennan Zhai, Ang Chen, Ruzica Piskac, Mahesh Balakrishnan, Bingchuan Tian, Bo Song, and Haoliang Zhang. 2020. Check before You Change: Preventing Correlated Failures in Service Updates. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 575--589. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/zhai"},{"key":"e_1_3_2_1_60_1","volume-title":"APKeep: Realtime Verification for Real Networks. In 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. 2020. APKeep: Realtime Verification for Real Networks. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 241--255. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/zhang-peng"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544264"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP55882.2022.9940438"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544247"}],"event":{"name":"ACM SIGCOMM '24: ACM SIGCOMM 2024 Conference","location":"Sydney NSW Australia","acronym":"ACM SIGCOMM '24","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2024 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651890.3672246","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651890.3672246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:12Z","timestamp":1750268952000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651890.3672246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,4]]},"references-count":62,"alternative-id":["10.1145\/3651890.3672246","10.1145\/3651890"],"URL":"https:\/\/doi.org\/10.1145\/3651890.3672246","relation":{},"subject":[],"published":{"date-parts":[[2024,8,4]]},"assertion":[{"value":"2024-08-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}