{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T05:46:00Z","timestamp":1780638360221,"version":"3.54.1"},"reference-count":44,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1900866"],"award-info":[{"award-number":["CNS-1900866"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1918187"],"award-info":[{"award-number":["CCF-1918187"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE\/ACM Trans. Networking"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1109\/tnet.2022.3176267","type":"journal-article","created":{"date-parts":[[2022,6,6]],"date-time":"2022-06-06T20:10:54Z","timestamp":1654546254000},"page":"2493-2504","source":"Crossref","is-referenced-by-count":8,"title":["Accelerating BGP Configuration Verification Through Reducing Cycles in SMT Constraints"],"prefix":"10.1109","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6097-5713","authenticated-orcid":false,"given":"Xiaozhe","family":"Shao","sequence":"first","affiliation":[{"name":"University of Massachusetts at Amherst, Amherst, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7890-9711","authenticated-orcid":false,"given":"Zibin","family":"Chen","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2052-9820","authenticated-orcid":false,"given":"Daniel","family":"Holcomb","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9017-5132","authenticated-orcid":false,"given":"Lixin","family":"Gao","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2012.2187924"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2014.6847989"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787508"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM41043.2020.9155235"},{"key":"ref31","author":"shao","year":"2022","journal-title":"BiNode"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2007.334"},{"key":"ref37","year":"2020","journal-title":"2020 Verizon Data Breach Investigations Report"},{"key":"ref36","year":"2021","journal-title":"BGP super-blunder How verizon today sparked a ‘cascading catastrophic failure’ that knackered cloudflare amazon etc"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342088"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"ref10","author":"dutt","year":"2017","journal-title":"BGP in the Data Center"},{"key":"ref40","first-page":"283","article-title":"Reduction-based formal analysis of BGP instances","author":"wang","year":"2021","journal-title":"Proc 18th Int Conf Tools Algorithms Construct Anal Syst (TACAS)"},{"key":"ref11","year":"2021","journal-title":"Update about the october 4th outage"},{"key":"ref12","first-page":"217","article-title":"Efficient network reachability analysis using a succinct control plane representation","author":"fayaz","year":"2016","journal-title":"Proc of USENIX Symp on Operating Systems Design and Implementation (OSDI)"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2007.892876"},{"key":"ref14","first-page":"469","article-title":"A general approach to network configuration analysis","author":"fogel","year":"2015","journal-title":"Proc 12th USENIX Conf Netw Syst Design Implement (NSDI)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/90.974523"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2567561.2567566"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/90.993304"},{"key":"ref19","first-page":"735","article-title":"Delta-net: Real-time network verification using atoms","author":"horn","year":"2017","journal-title":"Proc 14th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref28","year":"2021","journal-title":"Large Route Leaks"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2815675.2815712"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04918-2_17"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1402958.1402967"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230583"},{"key":"ref29","first-page":"953","article-title":"Plankton: Scalable network configuration verification through model checking","author":"prabhu","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"ref8","author":"chen","year":"4456","journal-title":"BGP route reflection An alternative to full mesh internal BGP (IBGP)"},{"key":"ref7","year":"2022","journal-title":"Inferred AS to Organization Mapping Dataset"},{"key":"ref2","first-page":"65","article-title":"Running BGP in data centers at scale","author":"abhashkumar","year":"2021","journal-title":"Proc 18th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref9","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc Theory Pract Softw 14th Int Conf Tools Algorithms Construct Anal Syst"},{"key":"ref1","first-page":"201","article-title":"Tiramisu: Fast multilayer network verification","author":"abhashkumar","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486019"},{"key":"ref22","first-page":"99","article-title":"Real time network policy checking using header space analysis","author":"kazemian","year":"2013","journal-title":"Proc USENIX NSDI"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"ref24","first-page":"15","article-title":"VeriFlow: Verifying network-wide invariants in real time","author":"khurshid","year":"2013","journal-title":"Proc 1st Workshop Hot Topics Softw Defined Netw (HotSDN ?12)"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984012"},{"key":"ref23","first-page":"113","article-title":"Header space analysis: Static checking for networks","author":"kazemian","year":"2012","journal-title":"Proc 9th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref44","first-page":"241","article-title":"Apkeep: Realtime verification for real networks","author":"zhang","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3229584.3229585"}],"container-title":["IEEE\/ACM Transactions on Networking"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/90\/9990997\/9789107-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/90\/9990997\/09789107.pdf?arnumber=9789107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T19:19:31Z","timestamp":1673896771000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9789107\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12]]},"references-count":44,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tnet.2022.3176267","relation":{},"ISSN":["1063-6692","1558-2566"],"issn-type":[{"value":"1063-6692","type":"print"},{"value":"1558-2566","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12]]}}}