{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T20:41:44Z","timestamp":1775680904122,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-17-C-0047"],"award-info":[{"award-number":["HR0011-17-C-0047"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1704336 1837030"],"award-info":[{"award-number":["1704336 1837030"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>The control plane of most computer networks runs distributed routing protocols that determine if and how traffic is forwarded. Errors in the configuration of network control planes frequently knock down critical online services, leading to economic damage for service providers and significant hardship for users. Validation via ahead-of-time simulation can help find configuration errors but such techniques are expensive or even intractable for large industrial networks. We explore the use of abstract interpretation to address this fundamental scaling challenge and find that the right abstractions can reduce the asymptotic complexity of network simulation. Based on this observation, we build a tool called ShapeShifter for reachability analysis. On a suite of 127 production networks from a large cloud provider, ShapeShifter provides an asymptotic improvement in runtime and memory over the state-of-the-art simulator. These gains come with a minimal loss in precision. Our abstract analysis accurately predicts reachability for all destinations for 95% of the networks and for most destinations for the remaining 5%. We also find that abstract interpretation of network control planes not only speeds up existing analyses but also facilitates new kinds of analyses. We illustrate this advantage through a new destination \"hijacking\" analysis for the border gateway protocol (BGP), the globally-deployed routing protocol.<\/jats:p>","DOI":"10.1145\/3371110","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Abstract interpretation of distributed network control planes"],"prefix":"10.1145","volume":"4","author":[{"given":"Ryan","family":"Beckett","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"given":"Ratul","family":"Mahajan","sequence":"additional","affiliation":[{"name":"University of Washington, USA \/ Intentionet, USA"}]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Mohammad Al-Fares Alexander Loukissas and Amin Vahdat. 2008. A Scalable Commodity Data Center Network Architecture. In SIGCOMM.  Mohammad Al-Fares Alexander Loukissas and Amin Vahdat. 2008. A Scalable Commodity Data Center Network Architecture. In SIGCOMM.","DOI":"10.1145\/1402958.1402967"},{"key":"e_1_2_2_2_1","volume-title":"Abstract Interpretation of Stateful Networks. In Static Analysis Symposium.","author":"Alpernas Kalev","year":"2018","unstructured":"Kalev Alpernas , Roman Manevich , Aurojit Panda , Mooly Sagiv , Scott Shenker , Sharon Shoham , and Yaron Velner . 2018 . Abstract Interpretation of Stateful Networks. In Static Analysis Symposium. Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, and Yaron Velner. 2018. Abstract Interpretation of Stateful Networks. In Static Analysis Symposium."},{"key":"e_1_2_2_3_1","unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL.  Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL."},{"key":"e_1_2_2_4_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2001","unstructured":"Thomas Ball , Rupak Majumdar , Todd D. Millstein , and Sriram K . Rajamani . 2001 . Automatic Predicate Abstraction of C Programs. In PLDI. 203\u2013213. Thomas Ball, Rupak Majumdar, Todd D. Millstein, and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In PLDI. 203\u2013213."},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM.  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM.","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control Plane Compression. In SIGCOMM. 476\u2013489.  Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control Plane Compression. In SIGCOMM. 476\u2013489.","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2003. A static analyzer for large safety-critical software. In PLDI. 196\u2013207.  Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2003. A static analyzer for large safety-critical software. In PLDI. 196\u2013207.","DOI":"10.1145\/780822.781153"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_2_9_1","volume-title":"12th International Conference, CAV, Proceedings. 154\u2013169","author":"Clarke Edmund M.","year":"2000","unstructured":"Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , and Helmut Veith . 2000 . Counterexample-Guided Abstraction Refinement. In Computer Aided Verification , 12th International Conference, CAV, Proceedings. 154\u2013169 . Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In Computer Aided Verification, 12th International Conference, CAV, Proceedings. 154\u2013169."},{"key":"e_1_2_2_10_1","unstructured":"Clos Network 2019. Clos network. https:\/\/en .wikipedia.org\/wiki\/Clos n etwork .  Clos Network 2019. Clos network. https:\/\/en .wikipedia.org\/wiki\/Clos n etwork ."},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 2nd International Symposium on Programming","author":"Cousot Patrick","year":"1976","unstructured":"Patrick Cousot and Radhia Cousot . 1976 . Static determination of dynamic properties of programs . In Proceedings of the 2nd International Symposium on Programming , Paris, France. Dunod, 106\u2013130. Patrick Cousot and Radhia Cousot. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming, Paris, France. Dunod, 106\u2013130."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In POPL. 84\u201396.  Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In POPL. 84\u201396.","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. 103\u2013116","author":"Daggitt Matthew L.","unstructured":"Matthew L. Daggitt , Alexander J. T. Gurney , and Timothy G. Griffin . 2018a. Asynchronous Convergence of Policy-rich Distributed Bellman-ford Routing Protocols . In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. 103\u2013116 . Matthew L. Daggitt, Alexander J. T. Gurney, and Timothy G. Griffin. 2018a. Asynchronous Convergence of Policy-rich Distributed Bellman-ford Routing Protocols. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. 103\u2013116."},{"key":"e_1_2_2_15_1","volume-title":"Griffin","author":"Daggitt Matthew L.","year":"2018","unstructured":"Matthew L. Daggitt , Alexander J. T. Gurney , and Timothy G . Griffin . 2018 b. Asynchronous Convergence of Policy-rich Distributed Bellman-ford Routing Protocols. In SIGCOMM. 103\u2013116. Matthew L. Daggitt, Alexander J. T. Gurney, and Timothy G. Griffin. 2018b. Asynchronous Convergence of Policy-rich Distributed Bellman-ford Routing Protocols. In SIGCOMM. 103\u2013116."},{"key":"e_1_2_2_16_1","first-page":"12","article-title":"Efficient Large-scale BGP","volume":"50","author":"Dimitropoulos Xenofontas A.","year":"2006","unstructured":"Xenofontas A. Dimitropoulos and George F. Riley . 2006 . Efficient Large-scale BGP Simulations. Comput. Netw. 50 , 12 (August 2006), 2013\u20132027. Xenofontas A. Dimitropoulos and George F. Riley. 2006. Efficient Large-scale BGP Simulations. Comput. Netw. 50, 12 (August 2006), 2013\u20132027.","journal-title":"Simulations. Comput. Netw."},{"key":"e_1_2_2_17_1","volume-title":"MRAI: Timing diversity can exponentially worsen BGP convergence. In INFOCOM. 2975\u20132983.","author":"Fabrikant A.","year":"2011","unstructured":"A. Fabrikant , U. Syed , and J. Rexford . 2011 . There\u2019s something about MRAI: Timing diversity can exponentially worsen BGP convergence. In INFOCOM. 2975\u20132983. A. Fabrikant, U. Syed, and J. Rexford. 2011. There\u2019s something about MRAI: Timing diversity can exponentially worsen BGP convergence. In INFOCOM. 2975\u20132983."},{"key":"e_1_2_2_18_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 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 OSDI."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00007-3"},{"key":"e_1_2_2_21_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 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 NSDI."},{"key":"e_1_2_2_22_1","volume-title":"Probabilistic NetKAT. In Proceedings of the 25th European Symposium on Programming Languages and Systems -","volume":"9632","author":"Foster Nate","year":"2016","unstructured":"Nate Foster , Dexter Kozen , Konstantinos Mamouras , Mark Reitblatt , and Alexandra Silva . 2016 . Probabilistic NetKAT. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632 . 282\u2013309. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632. 282\u2013309."},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Lixin Gao and Jennifer Rexford. 2000. Stable Internet Routing Without Global Coordination. In SIGMETRICS.  Lixin Gao and Jennifer Rexford. 2000. Stable Internet Routing Without Global Coordination. In SIGMETRICS.","DOI":"10.1145\/339331.339426"},{"key":"e_1_2_2_24_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 SIGCOMM.  Aaron Gember-Jacobson Raajay Viswanathan Aditya Akella and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. In SIGCOMM.","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Nick Giannarakis Ryan Beckett Ratul Mahajan and David Walker. 2019. Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement. 305\u2013323.  Nick Giannarakis Ryan Beckett Ratul Mahajan and David Walker. 2019. Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement. 305\u2013323.","DOI":"10.1007\/978-3-030-25543-5_18"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.993304"},{"key":"e_1_2_2_27_1","volume-title":"Metarouting. In Proceedings of the 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications. 1\u201312","author":"Timothy","unstructured":"Timothy G. Griffin and Jo\u00e4o Lu\u00eds Sobrinho. 2005 . Metarouting. In Proceedings of the 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications. 1\u201312 . Timothy G. Griffin and Jo\u00e4o Lu\u00eds Sobrinho. 2005. Metarouting. In Proceedings of the 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications. 1\u201312."},{"key":"e_1_2_2_28_1","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 NSDI. 99\u2013112.  Peyman Kazemian Michael Chang Hongyi Zeng George Varghese Nick McKeown and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In NSDI. 99\u2013112."},{"key":"e_1_2_2_29_1","unstructured":"Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI.  Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI."},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Ahmed Khurshid Xuan Zou Wenxuan Zhou Matthew Caesar and P. Brighten Godfrey. 2013. VeriFlow: Verifying NetworkWide Invariants in Real Time. In NSDI.  Ahmed Khurshid Xuan Zou Wenxuan Zhou Matthew Caesar and P. Brighten Godfrey. 2013. VeriFlow: Verifying NetworkWide Invariants in Real Time. In NSDI.","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_2_2_31_1","volume-title":"Daggitt and Timothy Griffin","author":"Matthew","year":"2018","unstructured":"Matthew L. Daggitt and Timothy Griffin . 2018 . Rate of Convergence of Increasing Path-Vector Routing Protocols. In ICNP. 335\u2013345. Matthew L. Daggitt and Timothy Griffin. 2018. Rate of Convergence of Increasing Path-Vector Routing Protocols. In ICNP. 335\u2013345."},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"P. Lapukhov A. Premji and J. Mitchell. 2015. Use of BGP for routing in large-scale data centers. Internet draft.  P. Lapukhov A. Premji and J. Mitchell. 2015. Use of BGP for routing in large-scale data centers. Internet draft.","DOI":"10.17487\/RFC7938"},{"key":"e_1_2_2_33_1","volume-title":"Confluently Persistent Sets and Maps. CoRR abs\/1301.3388","author":"Liljenzin Olle","year":"2013","unstructured":"Olle Liljenzin . 2013. Confluently Persistent Sets and Maps. CoRR abs\/1301.3388 ( 2013 ). Olle Liljenzin. 2013. Confluently Persistent Sets and Maps. CoRR abs\/1301.3388 (2013)."},{"key":"e_1_2_2_34_1","unstructured":"Nuno Lopes Nikolaj Bjorner Patrice Godefroid Karthick Jayaraman and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In NSDI.  Nuno Lopes Nikolaj Bjorner Patrice Godefroid Karthick Jayaraman and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In NSDI."},{"key":"e_1_2_2_35_1","volume-title":"Proc. of the 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 Proc. of the 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 Proc. of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"key":"e_1_2_2_36_1","unstructured":"Haohui Mai Ahmed Khurshid Rachit Agarwal Matthew Caesar P. Brighten Godfrey and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. In SIGCOMM.  Haohui Mai Ahmed Khurshid Rachit Agarwal Matthew Caesar P. Brighten Godfrey and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. In SIGCOMM."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_2_2_38_1","volume-title":"Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions","author":"Monat Rapha\u00ebl","unstructured":"Rapha\u00ebl Monat and Antoine Min\u00e9 . 2017. Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions . In Verification, Model Checking, and Abstract Interpretation, Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing , 386\u2013404. Rapha\u00ebl Monat and Antoine Min\u00e9. 2017. Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions. In Verification, Model Checking, and Abstract Interpretation, Ahmed Bouajjani and David Monniaux (Eds.). Springer International Publishing, 386\u2013404."},{"key":"e_1_2_2_39_1","article-title":"A Science of Network Configuration","volume":"1","author":"Narain Sanjay","year":"2016","unstructured":"Sanjay Narain , Dana Chee , Brian Coan , Ben Falchuk , Samuel Gordon , Jaewon Kang , Jonathan Kirsch , Aditya Naidu , Kaustubh Sinkar , and Simon Tsang . 2016 . A Science of Network Configuration . Journal of Cyber Security and Information Systems 1 , 4 (2016). Sanjay Narain, Dana Chee, Brian Coan, Ben Falchuk, Samuel Gordon, Jaewon Kang, Jonathan Kirsch, Aditya Naidu, Kaustubh Sinkar, and Simon Tsang. 2016. A Science of Network Configuration. Journal of Cyber Security and Information Systems 1, 4 (2016).","journal-title":"Journal of Cyber Security and Information Systems"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Gordon D. Plotkin Nikolaj Bj\u00f8rner Nuno P. Lopes Andrey Rybalchenko and George Varghese. 2016. Scaling Network Verification Using Symmetry and Surgery. In POPL.  Gordon D. Plotkin Nikolaj Bj\u00f8rner Nuno P. Lopes Andrey Rybalchenko and George Varghese. 2016. Scaling Network Verification Using Symmetry and Surgery. In POPL.","DOI":"10.1145\/2837614.2837657"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106989.3106991"},{"key":"e_1_2_2_42_1","unstructured":"Redistributing Routing Protocols 2012. Redistributing Routing Protocols. https:\/\/www .cisco.com\/c\/en\/us\/support\/docs\/ip\/ enhanced- interior- gateway- routing- protocol- eigrp\/8606- redist .html .  Redistributing Routing Protocols 2012. Redistributing Routing Protocols. https:\/\/www .cisco.com\/c\/en\/us\/support\/docs\/ip\/ enhanced- interior- gateway- routing- protocol- eigrp\/8606- redist .html ."},{"key":"e_1_2_2_43_1","unstructured":"D Roberts. 2018. It\u2019s been a week and customers are still mad at BB&amp;T. https:\/\/www .charlotteobserver.com\/news\/business\/ banking\/article202616124 .html .  D Roberts. 2018. It\u2019s been a week and customers are still mad at BB&amp;T. https:\/\/www .charlotteobserver.com\/news\/business\/ banking\/article202616124 .html ."},{"key":"e_1_2_2_44_1","volume-title":"Google cloud wobbles as workers patch wrong routers","author":"Sharwood Simon","unstructured":"Simon Sharwood . 2016. Google cloud wobbles as workers patch wrong routers . http:\/\/www .theregister.co.uk\/2016\/03\/01\/ google c loud w obbles a s w orkers p atc w rong r outers\/ . Simon Sharwood. 2016. Google cloud wobbles as workers patch wrong routers. http:\/\/www .theregister.co.uk\/2016\/03\/01\/ google c loud w obbles a s w orkers p atc w rong r outers\/ ."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2005.857111"},{"key":"e_1_2_2_46_1","unstructured":"Yevgenly Sverdlik. 2012. Microsoft: misconfigured network device led to Azure outage. http:\/\/ www .datacenterdynamics.com\/content-tracks\/servers-storage\/microsoft-misconfigured-network-device-ledto- azure- outage\/68312 .fullarticle .  Yevgenly Sverdlik. 2012. Microsoft: misconfigured network device led to Azure outage. http:\/\/ www .datacenterdynamics.com\/content-tracks\/servers-storage\/microsoft-misconfigured-network-device-ledto- azure- outage\/68312 .fullarticle ."},{"key":"e_1_2_2_47_1","unstructured":"Y Sverdlik. 2017. United Says IT Outage Resolved Dozen Flights Canceled Monday. https:\/\/www .datacenterknowledge.com\/ archives\/2017\/01\/23\/united- says- it- outage- resolved- dozen- flights- canceled- monday .  Y Sverdlik. 2017. United Says IT Outage Resolved Dozen Flights Canceled Monday. https:\/\/www .datacenterknowledge.com\/ archives\/2017\/01\/23\/united- says- it- outage- resolved- dozen- flights- canceled- monday ."},{"key":"e_1_2_2_48_1","unstructured":"Dylan Tweney. 2013. 5-minute outage costs Google $545 000 in revenue. https:\/\/venturebeat .com\/2013\/08\/16\/3-minuteoutage- costs- google- 545000- in- revenue\/ .  Dylan Tweney. 2013. 5-minute outage costs Google $545 000 in revenue. https:\/\/venturebeat .com\/2013\/08\/16\/3-minuteoutage- costs- google- 545000- in- revenue\/ ."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2012.2187924"},{"key":"e_1_2_2_51_1","unstructured":"Konstantin Weitz Doug Woos Emina Torlak Michael D. Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Formal Semantics and Automated Verification for the Border Gateway Protocol. In NetPL.  Konstantin Weitz Doug Woos Emina Torlak Michael D. Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Formal Semantics and Automated Verification for the Border Gateway Protocol. In NetPL."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371110","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371110","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371110"],"URL":"https:\/\/doi.org\/10.1145\/3371110","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}