{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,27]],"date-time":"2026-08-27T15:22:19Z","timestamp":1787844139212,"version":"build-2784847793"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030112448","type":"print"},{"value":"9783030112455","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_18","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T13:45:18Z","timestamp":1547127918000},"page":"386-408","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Fast BGP Simulation of Large Datacenters"],"prefix":"10.1007","author":[{"given":"Nuno P.","family":"Lopes","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Ad\u00e3o, P., Bozzato, C., Rossi, G.D., Focardi, R., Luccio, F.L.: Mignis: a semantic based tool for firewall configuration. In: CSF (2014)","DOI":"10.1109\/CSF.2014.32"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Al-Fares, M., Loukissas, A., Vahdat, A.: A scalable, commodity data center network architecture. In: SIGCOMM (2008)","DOI":"10.1145\/1402958.1402967"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated openflow infrastructures. In: SafeConfig (2010)","DOI":"10.1145\/1866898.1866905"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Alim, M.A., Griffin, T.G.: On the interaction of multiple routing algorithms. In: CoNEXT (2011)","DOI":"10.1145\/2079296.2079303"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL (2014)","DOI":"10.1145\/2535838.2535862"},{"key":"18_CR6","unstructured":"Andreyev, A.: Introducing data center fabric, the next-generation Facebook data center network (2014)"},{"issue":"6","key":"18_CR7","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/2666356.2594317","volume":"49","author":"Thomas Ball","year":"2014","unstructured":"Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: SIGCOMM (2017)","DOI":"10.1145\/3098822.3098834"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Don\u2019t mind the gap: bridging network-wide objectives and device-level configurations. In: SIGCOMM (2016)","DOI":"10.1145\/2934872.2934909"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Beckett, R., Mahajan, R., Millstein, T., Padhye, J., Walker, D.: Network configuration synthesis with abstract topologies. In: PLDI (2017)","DOI":"10.1145\/3062341.3062367"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-14977-6_2","volume-title":"Distributed Computing and Internet Technology","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Jayaraman, K.: Checking cloud contracts in Microsoft Azure. In: Natarajan, R., Barua, G., Patra, M.R. (eds.) ICDCIT 2015. LNCS, vol. 8956, pp. 21\u201332. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-14977-6_2"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-49052-6_4","volume-title":"Hardware and Software: Verification and Testing","author":"N Bj\u00f8rner","year":"2016","unstructured":"Bj\u00f8rner, N., Juniwal, G., Mahajan, R., Seshia, S.A., Varghese, G.: ddNF: an efficient data structure for header spaces. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 49\u201364. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_4"},{"issue":"1","key":"18_CR13","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/69.43410","volume":"1","author":"S Ceri","year":"1989","unstructured":"Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146\u2013166 (1989)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Dobrescu, M., Argyraki, K.: Software dataplane verification. In: NSDI (2014)","DOI":"10.1145\/2823400"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Dynerowicz, S., Griffin, T.G.: On the forwarding paths produced by internet routing algorithms. In: ICNP (2013)","DOI":"10.1109\/ICNP.2013.6733608"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.: SDNRacer: concurrency analysis for software-defined networks. In: PLDI (2016)","DOI":"10.1145\/2908080.2908124"},{"key":"18_CR17","unstructured":"Fayaz, S.K., et al.: Efficient network reachability analysis using a succinct control plane representation. In: OSDI (2016)"},{"key":"18_CR18","unstructured":"Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI (2005)"},{"issue":"2","key":"18_CR19","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1109\/TNET.2007.892876","volume":"15","author":"N Feamster","year":"2007","unstructured":"Feamster, N., Rexford, J.: Network-wide prediction of BGP routes. IEEE\/ACM Trans. Netw. 15(2), 253\u2013266 (2007)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR20","unstructured":"Fogel, A., et al.: A general approach to network configuration analysis. In: NSDI (2015)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Gao, L., Rexford, J.: Stable internet routing without global coordination. In: SIGMETRICS (2000)","DOI":"10.1145\/339331.339426"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Gember-Jacobson, A., Viswanathan, R., Akella, A., Mahajan, R.: Fast control plane analysis using an abstract representation. In: SIGCOMM (2016)","DOI":"10.1145\/2934872.2934876"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Greenberg, A., et al.: Vl2: a scalable and flexible data center network. In: SIGCOMM (2009)","DOI":"10.1145\/1592568.1592576"},{"issue":"2","key":"18_CR24","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/90.993304","volume":"10","author":"TG Griffin","year":"2002","unstructured":"Griffin, T.G., Shepherd, F.B., Wilfong, G.: The stable paths problem and interdomain routing. IEEE\/ACM Trans. Netw. 10(2), 232\u2013243 (2002)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Griffin, T.G., Shepherd, F.B., Wilfong, G.T.: Policy disputes in path-vector protocols. In: ICNP (1999)","DOI":"10.1109\/ICNP.1999.801912"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Griffin, T.G., Sobrinho, J.L.: Metarouting. In: SIGCOMM (2005)","DOI":"10.1145\/1080091.1080094"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Hallahan, W.T., Zhai, E., Piskac, R.: Automated repair by example for firewalls. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102263"},{"key":"18_CR28","unstructured":"Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: NSDI (2013)"},{"key":"18_CR29","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI (2012)"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: verifying network-wide invariants in real time. In: NSDI (2013)","DOI":"10.1145\/2342441.2342452"},{"key":"18_CR31","unstructured":"Lahiri, P., et al.: Routing design for large scale data centers: BGP is a better IGP. In: NANOG\u201955 (2012)"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Lapukhov, P., Premji, A., Mitchell, J.: RFC 7938: Use of BGP for Routing in Large-Scale Data Centers (2016)","DOI":"10.17487\/RFC7938"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-54233-7_144","volume-title":"Automata, Languages and Programming","author":"T Lengauer","year":"1991","unstructured":"Lengauer, T., Theune, D.: Efficient algorithms for path problems with general cost criteria. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 314\u2013326. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54233-7_144"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Liu, H., et al.: CrystalNet: faithfully emulating large production networks. In: SOSP (2017)","DOI":"10.1145\/3132747.3132759"},{"key":"18_CR35","unstructured":"Lloyd\u2019s. Failure of a top cloud service provider could cost US economy \\$15 billion (2018)"},{"key":"18_CR36","unstructured":"Lopes, N.P., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: NSDI (2015)"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. In: SIGCOMM (2011)","DOI":"10.1145\/2018436.2018470"},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD (2014)","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"18_CR39","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Bj\u00f8rner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: POPL (2016)","DOI":"10.1145\/2837614.2837657"},{"issue":"6","key":"18_CR40","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1109\/MNET.2005.1541716","volume":"19","author":"B Quoitin","year":"2005","unstructured":"Quoitin, B., Uhlig, S.: Modeling the routing of an autonomous system with C-BGP. IEEE Netw. 19(6), 12\u201319 (2005)","journal-title":"IEEE Netw."},{"key":"18_CR41","doi-asserted-by":"crossref","unstructured":"Rekhter, Y., Li, T., Hares, S.: RFC 4271: A Border Gateway Protocol 4 (BGP-4) (2006)","DOI":"10.17487\/rfc4271"},{"key":"18_CR42","unstructured":"Rusinovich, M.: TechEd 2013: Windows Azure Internals (2013)"},{"issue":"4","key":"18_CR43","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/TNET.2002.801397","volume":"10","author":"JL Sobrinho","year":"2002","unstructured":"Sobrinho, J.L.: Algebra and algorithms for QoS path computation and hop-by-hop routing in the internet. IEEE\/ACM Trans. Netw. 10(4), 541\u2013550 (2002)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR44","doi-asserted-by":"publisher","first-page":"1160","DOI":"10.1109\/TNET.2005.857111","volume":"13","author":"JL Sobrinho","year":"2005","unstructured":"Sobrinho, J.L.: An algebraic theory of dynamic network routing. IEEE\/ACM Trans. Netw. 13, 1160\u20131173 (2005)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR45","doi-asserted-by":"crossref","unstructured":"Subramanian, K., D\u2019Antoni, L., Akella, A.: Genesis: synthesizing forwarding tables in multi-tenant networks. In: POPL (2017)","DOI":"10.1145\/3009837.3009845"},{"key":"18_CR46","doi-asserted-by":"crossref","unstructured":"Wang, Y., et al.: TenantGuard: scalable runtime verification of cloud-wide VM-level network isolation. In: NDSS (2017)","DOI":"10.14722\/ndss.2017.23365"},{"key":"18_CR47","doi-asserted-by":"crossref","unstructured":"Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: OOPSLA (2016)","DOI":"10.1145\/2983990.2984012"},{"key":"18_CR48","doi-asserted-by":"crossref","unstructured":"Xie, G.G., et al.: On static reachability analysis of IP networks. In: INFOCOM (2005)","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"18_CR49","doi-asserted-by":"crossref","unstructured":"Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. In: ICNP (2013)","DOI":"10.1109\/ICNP.2013.6733614"},{"key":"18_CR50","unstructured":"Zhang, S., Mahmoud, A., Malik, S., Narain, S.: Verification and synthesis of firewalls using SAT and QBF. In: ICNP (2012)"},{"key":"18_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-319-02444-8_43","volume-title":"Automated Technology for Verification and Analysis","author":"S Zhang","year":"2013","unstructured":"Zhang, S., Malik, S.: SAT based verification of network data planes. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 496\u2013505. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_43"},{"key":"18_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-33386-6_1","volume-title":"Automated Technology for Verification and Analysis","author":"S Zhang","year":"2012","unstructured":"Zhang, S., Malik, S., McGeer, R.: Verification of computer switching networks: an overview. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 1\u201316. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_1"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T22:17:30Z","timestamp":1573683450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}