{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T20:41:42Z","timestamp":1775680902371,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T00:00:00Z","timestamp":1596067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"the National Key R&D Program of China","award":["2018YFB1800205"],"award-info":[{"award-number":["2018YFB1800205"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,30]]},"DOI":"10.1145\/3387514.3406217","type":"proceedings-article","created":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T22:35:31Z","timestamp":1596148531000},"page":"599-614","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Accuracy, Scalability, Coverage"],"prefix":"10.1145","author":[{"given":"Fangdan","family":"Ye","sequence":"first","affiliation":[{"name":"Tsinghua University and Alibaba Group"}]},{"given":"Da","family":"Yu","sequence":"additional","affiliation":[{"name":"Brown University and Alibaba Group"}]},{"given":"Ennan","family":"Zhai","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Hongqiang Harry","family":"Liu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Bingchuan","family":"Tian","sequence":"additional","affiliation":[{"name":"Nanjing University and Alibaba Group"}]},{"given":"Qiaobo","family":"Ye","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Chunsheng","family":"Wang","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Xin","family":"Wu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Tianchen","family":"Guo","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Cheng","family":"Jin","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Duncheng","family":"She","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Qing","family":"Ma","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Biao","family":"Cheng","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Hui","family":"Xu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Ming","family":"Zhang","sequence":"additional","affiliation":[{"name":"Alibaba Group"}]},{"given":"Zhiliang","family":"Wang","sequence":"additional","affiliation":[{"name":"Tsinghua University"}]},{"given":"Rodrigo","family":"Fonseca","sequence":"additional","affiliation":[{"name":"Brown University"}]}],"member":"320","published-online":{"date-parts":[[2020,7,30]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Tiramisu: Fast and General Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar , Aaron Gember-Jacobson , and Aditya Akella . 2020 . Tiramisu: Fast and General Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI). Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast and General Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_39"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v24i1.7545"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A general approach to network configuration verification. In ACM SIGCOMM (SIGCOMM).  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A general approach to network configuration verification. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control plane compression. In ACM SIGCOMM (SIGCOMM).  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control plane compression. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365609.3365866"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Ratul Mahajan Todd Millstein Jitendra Padhye and David Walker. 2016. Don't mind the gap: Bridging network-wide objectives and device-level configurations. In ACM SIGCOMM (SIGCOMM).  Ryan Beckett Ratul Mahajan Todd Millstein Jitendra Padhye and David Walker. 2016. Don't mind the gap: Bridging network-wide objectives and device-level configurations. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_3_2_2_8_1","volume-title":"15th USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Birkner R\u00fcdiger","unstructured":"R\u00fcdiger Birkner , Dana Drachsler-Cohen , Laurent Vanbever , and Martin T. Vechev . 2018. Net2Text: Query-guided summarization of network forwarding behaviors . In 15th USENIX Conference on Networked Systems Design and Implementation (NSDI). R\u00fcdiger Birkner, Dana Drachsler-Cohen, Laurent Vanbever, and Martin T. Vechev. 2018. Net2Text: Query-guided summarization of network forwarding behaviors. In 15th USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_9_1","volume-title":"17th USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Birkner R\u00fcdiger","unstructured":"R\u00fcdiger Birkner , Dana Drachsler-Cohen , Laurent Vanbever , and Martin T. Vechev . 2020. Config2Spec: Mining network specifications from network configurations . In 17th USENIX Conference on Networked Systems Design and Implementation (NSDI). R\u00fcdiger Birkner, Dana Drachsler-Cohen, Laurent Vanbever, and Martin T. Vechev. 2020. Config2Spec: Mining network specifications from network configurations. In 17th USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026895"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789770.2789803"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Aaron Gember-Jacobson Raajay Viswanathan Aditya Akella and Ratul Mahajan. 2016. Fast control plane analysis using an abstract representation. In ACM SIGCOMM (SIGCOMM).  Aaron Gember-Jacobson Raajay Viswanathan Aditya Akella and Ratul Mahajan. 2016. Fast control plane analysis using an abstract representation. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_2_14_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Horn Alex","unstructured":"Alex Horn , Ali Kheradmand , and Mukul R. Prasad . 2017. Delta-net: Real-time network verification using atoms . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI). Alex Horn, Ali Kheradmand, and Mukul R. Prasad. 2017. Delta-net: Real-time network verification using atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_15_1","volume-title":"Neha Milind Raje, and Parag Sharma.","author":"Jayaraman Karthick","year":"2019","unstructured":"Karthick Jayaraman , Nikolaj Bj\u00f8rner , Jitu Padhye , Amar Agrawal , Ashish Bhargava , Paul-Andre C. Bissonnette , Shane Foster , Andrew Helwer , Mark Kasten , Ivan Lee , Anup Namdhari , Haseeb Niaz , Aniruddha Parkhi , Hanukumar Pinnamraju , Adrian Power , Neha Milind Raje, and Parag Sharma. 2019 . Validating datacenters at scale. In ACM SIGCOMM (SIGCOMM) . Karthick Jayaraman, Nikolaj Bj\u00f8rner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C. Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. 2019. Validating datacenters at scale. In ACM SIGCOMM (SIGCOMM)."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281432"},{"key":"e_1_3_2_2_17_1","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Siva Kesava","year":"2020","unstructured":"Siva Kesava Reddy K., Alan Tang , Ryan Beckett , Karthick Jayaraman , Todd D. Millstein , Yuval Tamir , and George Varghese . 2020 . Finding network misconfigurations by automatic template inference . In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI). Siva Kesava Reddy K., Alan Tang, Ryan Beckett, Karthick Jayaraman, Todd D. Millstein, Yuval Tamir, and George Varghese. 2020. Finding network misconfigurations by automatic template inference. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_18_1","volume-title":"9th USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . 2012 . Header space analysis: Static checking for networks . In 9th USENIX Conference on Networked Systems Design and Implementation (NSDI). Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header space analysis: Static checking for networks. In 9th USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_19_1","volume-title":"10th USENIX Conference on Networked Systems Design and Implementation (NSDI).","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid , Xuan Zhou , Whenxuan Zhou , Matthew Caesar , and Philip Brighten Godfrey . 2013 . VeriFlow: Verifying network-wide invariants in real time . In 10th USENIX Conference on Networked Systems Design and Implementation (NSDI). Ahmed Khurshid, Xuan Zhou, Whenxuan Zhou, Matthew Caesar, and Philip Brighten Godfrey. 2013. VeriFlow: Verifying network-wide invariants in real time. In 10th USENIX Conference on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_3_2_2_21_1","volume-title":"12th USENIX Symposium on Networked System Design and Implementation (NSDI).","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 System Design and Implementation (NSDI). 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 System Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_22_1","volume-title":"Fast BGP Simulation of Large Datacenters. In 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).","author":"Nuno","unstructured":"Nuno P. Lopes and Andrey Rybalchenko. 2019 . Fast BGP Simulation of Large Datacenters. In 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Nuno P. Lopes and Andrey Rybalchenko. 2019. Fast BGP Simulation of Large Datacenters. In 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837657"},{"key":"e_1_3_2_2_24_1","volume-title":"17th USENIX Symposium on Networked System Design and Implementation (NSDI).","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 17th USENIX Symposium on Networked System Design and Implementation (NSDI). Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. In 17th USENIX Symposium on Networked System Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2005.1541716"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"J. Scudder R. Fernando and S. Stuart. 2016. BGP Monitoring Protocol (BMP). RFC 7854. IETF. http:\/\/tools.ietf.org\/rfc\/rfc7854.txt  J. Scudder R. Fernando and S. Stuart. 2016. BGP Monitoring Protocol (BMP). RFC 7854. IETF. http:\/\/tools.ietf.org\/rfc\/rfc7854.txt","DOI":"10.17487\/RFC7854"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Radu Stoenescu Matei Popovici Lorina Negreanu and Costin Raiciu. 2016. SymNet: Scalable symbolic execution for modern networks. In ACM SIGCOMM (SIGCOMM).  Radu Stoenescu Matei Popovici Lorina Negreanu and Costin Raiciu. 2016. SymNet: Scalable symbolic execution for modern networks. In ACM SIGCOMM (SIGCOMM).","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_2_28_1","volume-title":"Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, Da Yu, Chen Tian, Haitao Zheng, and Ben Y. Zhao.","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, Da Yu, Chen Tian, Haitao Zheng, and Ben Y. Zhao. 2019 . Safely and automatically updating in-network ACL configurations with intent language. In ACM SIGCOMM (SIGCOMM) . Bingchuan Tian, Xinyi Zhang, Ennan Zhai, Hongqiang Harry Liu, Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, Da Yu, Chen Tian, Haitao Zheng, and Ben Y. Zhao. 2019. Safely and automatically updating in-network ACL configurations with intent language. In ACM SIGCOMM (SIGCOMM)."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_2_30_1","volume-title":"16th USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Yu Da","year":"2019","unstructured":"Da Yu , Yibo Zhu , Behnaz Arzani , Rodrigo Fonseca , Tianrong Zhang , Karl Deng , and Lihua Yuan . 2019 . dShark: A general, easy to program and scalable framework for analyzing in-network packet traces . In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI). Da Yu, Yibo Zhu, Behnaz Arzani, Rodrigo Fonseca, Tianrong Zhang, Karl Deng, and Lihua Yuan. 2019. dShark: A general, easy to program and scalable framework for analyzing in-network packet traces. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413205"},{"key":"e_1_3_2_2_32_1","volume-title":"17th USENIX Symposium on Networked System Design and Implementation (NSDI).","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 System Design and Implementation (NSDI). 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 System Design and Implementation (NSDI)."}],"event":{"name":"SIGCOMM '20: Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication","location":"Virtual Event USA","acronym":"SIGCOMM '20","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387514.3406217","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387514.3406217","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:36Z","timestamp":1750200096000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387514.3406217"}},"subtitle":["A Practical Configuration Verifier on a Global WAN"],"short-title":[],"issued":{"date-parts":[[2020,7,30]]},"references-count":32,"alternative-id":["10.1145\/3387514.3406217","10.1145\/3387514"],"URL":"https:\/\/doi.org\/10.1145\/3387514.3406217","relation":{},"subject":[],"published":{"date-parts":[[2020,7,30]]},"assertion":[{"value":"2020-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}