{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T10:27:33Z","timestamp":1769509653495,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":41,"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":"Eidgen\u00f6ssische Technische Hochschule Z\u00fcrich","award":["ETH-03 19-2"],"award-info":[{"award-number":["ETH-03 19-2"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,30]]},"DOI":"10.1145\/3387514.3405900","type":"proceedings-article","created":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T22:35:31Z","timestamp":1596148531000},"page":"750-764","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Probabilistic Verification of Network Configurations"],"prefix":"10.1145","author":[{"given":"Samuel","family":"Steffen","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Timon","family":"Gehr","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Petar","family":"Tsankov","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Laurent","family":"Vanbever","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2020,7,30]]},"reference":[{"key":"e_1_3_2_2_1_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 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_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/633025.633048"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_2_5_1","volume-title":"Pattern recognition and machine learning","author":"Bishop Christopher M.","unstructured":"Christopher M. Bishop . 2006. Pattern recognition and machine learning . Springer , New York . Christopher M. Bishop. 2006. Pattern recognition and machine learning. Springer, New York."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342069"},{"key":"e_1_3_2_2_7_1","volume-title":"Interval Estimation for a Binomial Proportion. Statist. Sci. 16, 2 (05","author":"Brown Lawrence D.","year":"2001","unstructured":"Lawrence D. Brown , T. Tony Cai , and Anirban DasGupta . 2001. Interval Estimation for a Binomial Proportion. Statist. Sci. 16, 2 (05 2001 ), 101--133. https:\/\/doi.org\/10.1214\/ss\/1009213286 Lawrence D. Brown, T. Tony Cai, and Anirban DasGupta. 2001. Interval Estimation for a Binomial Proportion. Statist. Sci. 16, 2 (05 2001), 101--133. https:\/\/doi.org\/10.1214\/ss\/1009213286"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3366697"},{"key":"e_1_3_2_2_9_1","volume-title":"UnderstandingBGPnext-hopdiversity. In2011IEEEConferenceonComputer Communications Workshops (INFOCOM WKSHPS). 846--851","author":"Choi Jaeyoung","year":"2011","unstructured":"Jaeyoung Choi , Jong Han Park , Pei chun Cheng , Dorian Kim , and Lixia Zhang . 2011 . UnderstandingBGPnext-hopdiversity. In2011IEEEConferenceonComputer Communications Workshops (INFOCOM WKSHPS). 846--851 . https:\/\/doi.org\/10.1109\/INFCOMW.2011.5928930 Jaeyoung Choi, Jong Han Park, Pei chun Cheng, Dorian Kim, and Lixia Zhang. 2011. UnderstandingBGPnext-hopdiversity. In2011IEEEConferenceonComputer Communications Workshops (INFOCOM WKSHPS). 846--851. https:\/\/doi.org\/10.1109\/INFCOMW.2011.5928930"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/NOMS.2010.5488479"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1996.10476956"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026895"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2007.892876"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2010.01.011"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2008.4697049"},{"key":"e_1_3_2_2_16_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. 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."},{"key":"e_1_3_2_2_17_1","volume-title":"Programming Languages and Systems (ESOP '16)","author":"Foster Nate","unstructured":"Nate Foster , Dexter Kozen , Konstantinos Mamouras , Mark Reitblatt , and Alexandra Silva . 2016. Probabilistic NetKAT . In Programming Languages and Systems (ESOP '16) , Peter Thiemann (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 282--309. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Programming Languages and Systems (ESOP '16), Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 282--309."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018477"},{"key":"e_1_3_2_2_21_1","volume-title":"Cisco ISP essentials","author":"Greene Barry Raveendran","unstructured":"Barry Raveendran Greene and Philip Smith . 2002. Cisco ISP essentials . Cisco Press . Barry Raveendran Greene and Philip Smith. 2002. Cisco ISP essentials. Cisco Press."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/633025.633028"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_3_2_2_24_1","first-page":"99","article-title":"Real Time Network Policy Checking Using Header Space Analysis. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX","author":"Kazemian Peyman","year":"2013","unstructured":"Peyman Kazemian , Michael Chang , Hongyi Zeng , George Varghese , Nick McKeown , and Scott Whyte . 2013 . Real Time Network Policy Checking Using Header Space Analysis. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX , Lombard , IL , 99 -- 111 . Peyman Kazemian, Michael Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX, Lombard, IL, 99--111.","journal-title":"Lombard"},{"key":"e_1_3_2_2_25_1","volume-title":"Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12)","author":"Kazemian Peyman","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . 2012. Header Space Analysis: Static Checking for Networks . In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12) . USENIX , San Jose, CA , 113--126. Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12). USENIX, San Jose, CA, 113--126."},{"key":"e_1_3_2_2_26_1","first-page":"15","article-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX","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 Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX , Lombard , IL , 15 -- 27 . Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13). USENIX, Lombard, IL, 15--27.","journal-title":"Lombard"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_2_28_1","unstructured":"Pierre Simon Laplace. 1812. Th\u00e9orie analytique des probabilit\u00e9s. Ve. Courcier.  Pierre Simon Laplace. 1812. Th\u00e9orie analytique des probabilit\u00e9s. Ve. Courcier."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1644893.1644937"},{"key":"e_1_3_2_2_31_1","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 . 2020 . Plankton: Scalable network configuration verification through model checking . In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI '20) . USENIX Association, Santa Clara, CA, 953--967. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/prabhu 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 Systems Design and Implementation (NSDI '20). USENIX Association, Santa Clara, CA, 953--967. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/prabhu"},{"key":"e_1_3_2_2_32_1","first-page":"12","article-title":"Modeling the routing of an autonomous systemwith C-BGP","volume":"19","author":"Quoitin Bruno","year":"2005","unstructured":"Bruno Quoitin and Steve Uhlig . 2005 . Modeling the routing of an autonomous systemwith C-BGP . IEEEnetwork 19 , 6 (2005), 12 -- 19 . Bruno Quoitin and Steve Uhlig. 2005. Modeling the routing of an autonomous systemwith C-BGP. IEEEnetwork 19, 6 (2005), 12--19.","journal-title":"IEEEnetwork"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Y. Rekhter T. Li andS. Hares. 2006. ABorder GatewayProtocol 4 (BGP-4). RFC 4271 (Draft Standard). http:\/\/www.ietf.org\/rfc\/rfc4271.txt  Y. Rekhter T. Li andS. Hares. 2006. ABorder GatewayProtocol 4 (BGP-4). RFC 4271 (Draft Standard). http:\/\/www.ietf.org\/rfc\/rfc4271.txt","DOI":"10.17487\/rfc4271"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/637201.637232"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009843"},{"key":"e_1_3_2_2_36_1","volume-title":"Network Operations and Management Symposium (NOMS '02)","author":"Steinder M.","unstructured":"M. Steinder and A. S. Sethi . 2002. End-to-end service failure diagnosis using belief networks . In Network Operations and Management Symposium (NOMS '02) . 375--390. M. Steinder and A. S. Sethi. 2002. End-to-end service failure diagnosis using belief networks. In Network Operations and Management Symposium (NOMS '02). 375--390."},{"key":"e_1_3_2_2_37_1","volume-title":"Proceedings of the Twenty-First Annual Joint Conference of the IEEE Computer and Communications Societies","volume":"1","author":"Steinder M.","unstructured":"M. Steinder and A. S. Sethi . 2002. Increasing robustness of fault localization through analysis of lost, spurious, and positive symptoms . In Proceedings of the Twenty-First Annual Joint Conference of the IEEE Computer and Communications Societies , Vol. 1 . 322-331 vol.1. M. Steinder and A. S. Sethi. 2002. Increasing robustness of fault localization through analysis of lost, spurious, and positive symptoms. In Proceedings of the Twenty-First Annual Joint Conference of the IEEE Computer and Communications Societies, Vol. 1. 322-331 vol.1."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851182.1851220"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2013.2296330"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_2_41_1","first-page":"1","article-title":"Exploiting Causal Independence in Bayesian Network Inference","volume":"5","author":"Zhang Nevin Lianwen","year":"1996","unstructured":"Nevin Lianwen Zhang and David Poole . 1996 . Exploiting Causal Independence in Bayesian Network Inference . J. Artif. Int. Res. 5 , 1 (Dec. 1996), 301--328. http:\/\/dl.acm.org\/citation.cfm?id=1622756.1622765 Nevin Lianwen Zhang and David Poole. 1996. Exploiting Causal Independence in Bayesian Network Inference. J. Artif. Int. Res. 5, 1 (Dec. 1996), 301--328. http:\/\/dl.acm.org\/citation.cfm?id=1622756.1622765","journal-title":"J. Artif. Int. Res."}],"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.3405900","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387514.3405900","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.3405900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,30]]},"references-count":41,"alternative-id":["10.1145\/3387514.3405900","10.1145\/3387514"],"URL":"https:\/\/doi.org\/10.1145\/3387514.3405900","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"}}]}}