{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T06:31:35Z","timestamp":1783146695810,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,19]],"date-time":"2017-10-19T00:00:00Z","timestamp":1508371200000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["FA8750-12-2-0107, FA8750-12-C-0174, FA8750-15-C-0010, FA8750-16-2-0032"],"award-info":[{"award-number":["FA8750-12-2-0107, FA8750-12-C-0174, FA8750-15-C-0010, FA8750-16-2-0032"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["DGE-1256082"],"award-info":[{"award-number":["DGE-1256082"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,10,19]]},"DOI":"10.1145\/2983990.2984012","type":"proceedings-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T11:58:54Z","timestamp":1476964734000},"page":"765-780","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Scalable verification of border gateway protocol configurations with an SMT solver"],"prefix":"10.1145","author":[{"given":"Konstantin","family":"Weitz","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Doug","family":"Woos","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arvind","family":"Krishnamurthy","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_1_3_1","unstructured":"BelW\u00fc. https:\/\/www.belwue.de\/."},{"key":"e_1_3_2_1_4_1","unstructured":"BGP Feature Guide for the OCX Series. 2015."},{"key":"e_1_3_2_1_5_1","unstructured":"M. Brown. Pakistan hijacks YouTube. http:\/\/research. dyn.com\/2008\/02\/pakistan-hijacks-youtube-1\/. 2008."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855756"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_8_1","volume-title":"http:\/\/research. dyn.com\/2010\/11\/chinas-18-minute-mystery\/","author":"Cowie J.","year":"2010","unstructured":"J. Cowie. China\u2019s 18-Minute Mystery. http:\/\/research. dyn.com\/2010\/11\/chinas-18-minute-mystery\/. 2010."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2616448.2616459"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251203.1251207"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789770.2789803"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034812"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/339331.339426"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2668152.2668966"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_1_18_1","unstructured":"International Telecommunication Union Statistics. 2014."},{"key":"e_1_3_2_1_19_1","unstructured":"Internet2 Configurations. http:\/\/vn.grnoc.iu.edu\/Internet2\/ configs\/configs.html."},{"key":"e_1_3_2_1_20_1","unstructured":"Internet2 Fees. http : \/ \/ www. internet2. edu \/ about - us \/ membership\/."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032345"},{"key":"e_1_3_2_1_22_1","volume-title":"Firewall Filters, and Traffic Policers Feature Guide for Routing Devices.","year":"2016","unstructured":"Junos OS: Routing Policies, Firewall Filters, and Traffic Policers Feature Guide for Routing Devices. 2016."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2228298.2228311"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429125"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_26_1","volume-title":"This is Boogie 2. Tech. rep","author":"Leino K. R. M.","year":"2008","unstructured":"K. R. M. Leino. This is Boogie 2. Tech. rep. 2008."},{"key":"e_1_3_2_1_27_1","unstructured":"D. Madory. Chinese Routing Errors Redirect Russian Traffic. http:\/\/research.dyn.com\/2014\/11\/chinese-routingerrors-redirect-russian-traffic\/. 2014."},{"key":"e_1_3_2_1_28_1","volume-title":"U.S. web traffic. http : \/ \/ www. cnn. com \/ 2010 \/ US \/ 11 \/ 17 \/ websites. chinese.servers\/.","author":"McConnell D.","year":"2010","unstructured":"D. McConnell. Chinese company \u2018hijacked\u2019 U.S. web traffic. http : \/ \/ www. cnn. com \/ 2010 \/ US \/ 11 \/ 17 \/ websites. chinese.servers\/. 2010."},{"key":"e_1_3_2_1_29_1","volume-title":"Application of Routing Policy Specification Language (RPSL) on the Internet","author":"Meyer D.","year":"1997","unstructured":"D. Meyer, J. Schmitz, and C. Alaettinoglu. Application of Routing Policy Specification Language (RPSL) on the Internet. 1997."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103685"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2005.1541716"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.17487\/rfc4271"},{"key":"e_1_3_2_1_33_1","unstructured":"L. Schaefer. Deutsche Telekom: \u2019Internet data made in Germany should stay in Germany\u2019. http:\/\/www.dw. com\/en\/deutsche-telekom-internet-data-made-in-germanyshould-stay-in-germany\/a-17165891. 2013."},{"key":"e_1_3_2_1_34_1","unstructured":"Selfnet. https:\/\/selfnet.de\/."},{"key":"e_1_3_2_1_35_1","volume-title":"2010 Report to Congress of the U.S.\u2013China Economic and Security Review Commission","author":"Slane D.","year":"2010","unstructured":"D. Slane. 2010 Report to Congress of the U.S.\u2013China Economic and Security Review Commission. 2010."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851182.1851220"},{"key":"e_1_3_2_1_41_1","volume-title":"Bagpipe: Verified BGP Configuration Checking. Tech. rep","author":"Weitz K.","year":"2016","unstructured":"K. Weitz et al. Bagpipe: Verified BGP Configuration Checking. Tech. rep. 2016."}],"event":{"name":"SPLASH '16: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Amsterdam Netherlands","acronym":"SPLASH '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983990.2984012","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2983990.2984012","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2983990.2984012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:24:37Z","timestamp":1763457877000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983990.2984012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,19]]},"references-count":41,"alternative-id":["10.1145\/2983990.2984012","10.1145\/2983990"],"URL":"https:\/\/doi.org\/10.1145\/2983990.2984012","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022671.2984012","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,10,19]]},"assertion":[{"value":"2016-10-19","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}