{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T16:06:37Z","timestamp":1782835597636,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:00:00Z","timestamp":1604448000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Natural Science Foundation of China","award":["61772412 61802168"],"award-info":[{"award-number":["61772412 61802168"]}]},{"name":"National Science Foundation","award":["1763512"],"award-info":[{"award-number":["1763512"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,4]]},"DOI":"10.1145\/3422604.3425936","type":"proceedings-article","created":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:50:36Z","timestamp":1604019036000},"page":"81-87","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Incremental Network Configuration Verification"],"prefix":"10.1145","author":[{"given":"Peng","family":"Zhang","sequence":"first","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuhao","family":"Huang","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Gember-Jacobson","sequence":"additional","affiliation":[{"name":"Colgate University, Hamilton, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wenbo","family":"Shi","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xu","family":"Liu","sequence":"additional","affiliation":[{"name":"Xi'an Jiaotong University, Xi'an, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongkun","family":"Yang","sequence":"additional","affiliation":[{"name":"Unaffiliated, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhiqiang","family":"Zuo","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. Batfish. https:\/\/github.com\/batfish\/batfish.  [n.d.]. Batfish. https:\/\/github.com\/batfish\/batfish."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. Differential Datalog (DDlog). https:\/\/github.com\/vmware\/differentialdatalog.  [n.d.]. Differential Datalog (DDlog). https:\/\/github.com\/vmware\/differentialdatalog."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. How incremental solving works in Z3? https:\/\/stackoverflow.com\/ questions\/16422018\/how-incremental-solving-works-in-z3.  [n.d.]. How incremental solving works in Z3? https:\/\/stackoverflow.com\/ questions\/16422018\/how-incremental-solving-works-in-z3."},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. Human Factors Are Causing Most Of Todays Network Outages And Vulnerabilities. https:\/\/tinyurl.com\/ya7qy7nm.  [n.d.]. Human Factors Are Causing Most Of Todays Network Outages And Vulnerabilities. https:\/\/tinyurl.com\/ya7qy7nm."},{"key":"e_1_3_2_1_5_1","volume-title":"Tiramisu: Fast and General Network Verification. In USENIX NSDI.","author":"Abhashkumar Anubhavnidhi","year":"2020"},{"key":"e_1_3_2_1_6_1","volume-title":"Todd J Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L Veldhuizen, and Geoffrey Washburn.","author":"Aref Molham","year":"2015"},{"key":"e_1_3_2_1_7_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.  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A general approach to network configuration verification. In ACM SIGCOMM.","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control plane compression. In ACM SIGCOMM.  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control plane compression. In ACM SIGCOMM.","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2020. Abstract interpretation of distributed network control planes. In ACM POPL.  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2020. Abstract interpretation of distributed network control planes. In ACM POPL.","DOI":"10.1145\/3371110"},{"key":"e_1_3_2_1_10_1","unstructured":"Theophilus Benson Aditya Akella and David Maltz. 2009. Unraveling the Complexity of Network Management. In USENIX NSDI.  Theophilus Benson Aditya Akella and David Maltz. 2009. Unraveling the Complexity of Network Management. In USENIX NSDI."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Theophilus Benson Aditya Akella and Aman Shaikh. 2011. Demystifying Configuration Challenges and Trade-offs in Network-based ISP Services. In ACM SIGCOMM.  Theophilus Benson Aditya Akella and Aman Shaikh. 2011. Demystifying Configuration Challenges and Trade-offs in Network-based ISP Services. In ACM SIGCOMM.","DOI":"10.1145\/2018436.2018471"},{"key":"e_1_3_2_1_12_1","unstructured":"R\u00fcdiger Birkner Dana Drachsler-Cohen Laurent Vanbever and Martin Vechev. 2020. Config2Spec: Mining Network Specifications from Network Configurations. In USENIX NSDI.  R\u00fcdiger Birkner Dana Drachsler-Cohen Laurent Vanbever and Martin Vechev. 2020. Config2Spec: Mining Network Specifications from Network Configurations. In USENIX NSDI."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_14_1","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 USENIX OSDI.  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 USENIX OSDI."},{"key":"e_1_3_2_1_15_1","unstructured":"Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In USENIX NSDI.  Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In USENIX NSDI."},{"key":"e_1_3_2_1_16_1","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 USENIX NSDI.  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 USENIX NSDI."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Aaron Gember-Jacobson Aditya Akella Ratul Mahajan and Hongqiang Harry Liu. 2017. Automatically repairing network control planes using an abstract representation. In ACM SOSP.  Aaron Gember-Jacobson Aditya Akella Ratul Mahajan and Hongqiang Harry Liu. 2017. Automatically repairing network control planes using an abstract representation. In ACM SOSP.","DOI":"10.1145\/3132747.3132753"},{"key":"e_1_3_2_1_18_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.  Aaron Gember-Jacobson Raajay Viswanathan Aditya Akella and Ratul Mahajan. 2016. Fast control plane analysis using an abstract representation. In ACM SIGCOMM.","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Aaron Gember-Jacobson Wenfei Wu Xiujun Li Aditya Akella and Ratul Mahajan. 2015. Management Plane Analytics. In ACM SIGCOMM IMC.  Aaron Gember-Jacobson Wenfei Wu Xiujun Li Aditya Akella and Ratul Mahajan. 2015. Management Plane Analytics. In ACM SIGCOMM IMC.","DOI":"10.1145\/2815675.2815684"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_18"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.993304"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Timothy G Griffin and Jo\u00e4o Lu\u00eds Sobrinho. 2005. Metarouting. In ACM SIGCOMM.  Timothy G Griffin and Jo\u00e4o Lu\u00eds Sobrinho. 2005. Metarouting. In ACM SIGCOMM.","DOI":"10.1145\/1080091.1080094"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Timothy G Griffin and Gordon Wilfong. 1999. An analysis of BGP convergence properties. In ACM SIGCOMM.  Timothy G Griffin and Gordon Wilfong. 1999. An analysis of BGP convergence properties. In ACM SIGCOMM.","DOI":"10.1145\/316188.316231"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_25_1","volume-title":"Delta-net: Real-time Network Verification Using Atoms. In USENIX NSDI.","author":"Horn Alex","year":"2017"},{"key":"e_1_3_2_1_26_1","volume-title":"Neha Milind Raje, and Parag Sharma.","author":"Jayaraman Karthick","year":"2019"},{"key":"e_1_3_2_1_27_1","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 USENIX NSDI.  Peyman Kazemian Michael Chan Hongyi Zeng George Varghese Nick McKeown and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In USENIX NSDI."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Ahmed Khurshid Wenxuan Zhou Matthew Caesar and P Godfrey. 2013. VeriFlow: Verifying network-wide invariants in real time. In USENIX NSDI.  Ahmed Khurshid Wenxuan Zhou Matthew Caesar and P Godfrey. 2013. VeriFlow: Verifying network-wide invariants in real time. In USENIX NSDI.","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_3_2_1_29_1","unstructured":"Hyojoon Kim Theophilus Benson Aditya Akella and Nick Feamster. 2011. The evolution of network configuration: a tale of two campuses. In ACM SIGCOMM IMC.  Hyojoon Kim Theophilus Benson Aditya Akella and Nick Feamster. 2011. The evolution of network configuration: a tale of two campuses. In ACM SIGCOMM IMC."},{"key":"e_1_3_2_1_30_1","volume-title":"Kinetic: Verifiable dynamic network control. In USENIX NSDI.","author":"Kim Hyojoon","year":"2015"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341561.3349591"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229584.3229585"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_18"},{"key":"e_1_3_2_1_34_1","volume-title":"Rebecca Isaacs, and Michael Isard.","author":"McSherry Frank","year":"2013"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855698.1855704"},{"key":"e_1_3_2_1_36_1","unstructured":"Santhosh Prabhu. [n.d.]. Personal communication.  Santhosh Prabhu. [n.d.]. Personal communication."},{"key":"e_1_3_2_1_37_1","volume-title":"Plankton: Scalable network configuration verification through model checking. In USENIX NSDI.","author":"Prabhu Santhosh","year":"2020"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2005.1541716"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2005.857111"},{"key":"e_1_3_2_1_40_1","volume-title":"Robotron: Top-down Network Management at Facebook Scale. In ACM SIGCOMM.","author":"Eric Sung Yu-Wei","year":"2016"},{"key":"e_1_3_2_1_41_1","volume-title":"Qiaobo Ye, Chunsheng Wang, Xin Wu, Zhiming Ji, Yihong Sang, Ming Zhang, et almbox.","author":"Tian Bingchuan","year":"2019"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Konstantin Weitz Doug Woos Emina Torlak Michael D Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Scalable verification of border gateway protocol configurations with an SMT solver. In ACM OOPSLA.  Konstantin Weitz Doug Woos Emina Torlak Michael D Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Scalable verification of border gateway protocol configurations with an SMT solver. In ACM OOPSLA.","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_43_1","volume-title":"Real-time verification of network properties using Atomic Predicates","author":"Yang Hongkun"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"e_1_3_2_1_45_1","volume-title":"Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, et almbox.","author":"Ye Fangdan","year":"2020"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Hongyi Zeng Peyman Kazemian George Varghese and Nick McKeown. 2012. Automatic Test Packet Generation. In ACM CoNEXT.  Hongyi Zeng Peyman Kazemian George Varghese and Nick McKeown. 2012. Automatic Test Packet Generation. In ACM CoNEXT.","DOI":"10.1145\/2413176.2413205"},{"key":"e_1_3_2_1_47_1","unstructured":"Peng Zhang Xu Liu Hongkun Yang Ning Kang Zhengchang Gu and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In USENIX NSDI.  Peng Zhang Xu Liu Hongkun Yang Ning Kang Zhengchang Gu and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In USENIX NSDI."}],"event":{"name":"HotNets '20: The 19th ACM Workshop on Hot Topics in Networks","location":"Virtual Event USA","acronym":"HotNets '20","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 19th ACM Workshop on Hot Topics in Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422604.3425936","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3422604.3425936","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3422604.3425936","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:29Z","timestamp":1750195889000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422604.3425936"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,4]]},"references-count":47,"alternative-id":["10.1145\/3422604.3425936","10.1145\/3422604"],"URL":"https:\/\/doi.org\/10.1145\/3422604.3425936","relation":{},"subject":[],"published":{"date-parts":[[2020,11,4]]},"assertion":[{"value":"2020-11-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}