{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,25]],"date-time":"2026-07-25T16:04:19Z","timestamp":1784995459813,"version":"3.55.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633893","type":"print"},{"value":"9783319633909","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_14","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"261-281","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":61,"title":["Network-Wide Configuration Synthesis"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"El-Hassany","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petar","family":"Tsankov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Vanbever","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"14_CR1","unstructured":"Ryall, J.: Facebook, Tinder, Instagram suffer widespread issues. http:\/\/mashable.com\/2015\/01\/27\/facebook-tinder-instagram-issues\/"},{"key":"14_CR2","unstructured":"Juniper Networks. What\u2019s Behind Network Downtime? Proactive Steps to Reduce Human Error and Improve Availability of Networks. Technical report, May 2008"},{"key":"14_CR3","unstructured":"BGPmon. Internet prefixes monitoring. http:\/\/www.bgpmon.net\/blog\/"},{"key":"14_CR4","unstructured":"Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., Millstein, T.: A general approach to network configuration analysis. In: NSDI (2015)"},{"key":"14_CR5","unstructured":"Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI (2005)"},{"key":"14_CR6","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The margrave tool for firewall analysis. In: LISA (2010)"},{"key":"14_CR7","unstructured":"Yuan, L., Chen, H., Mai, J., Chuah, C.-N., Su, Z., Mohapatra, P.: FIREMAN: a toolkit for firewall modeling and analysis. In: S&P (2006)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Vanbever, L., Quoitin, B., Bonaventure, O.: A hierarchical model for BGP routing policies. In: ACM SIGCOMM PRESTO (2009)","DOI":"10.1145\/1592631.1592646"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Chen, X., Mao, M., Van der Merwe, J.: PACMAN: a platform for automated and controlled network operations and configuration management. In: CoNEXT (2009)","DOI":"10.1145\/1658939.1658971"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Enck, W., Moyer, T., McDaniel, P., Sen, S., Sebos, P., Spoerel, S., Greenberg, A., Sung, Y.-W.E., Rao, S., Aiello, W.: Configuration management at massive scale: system design and experience. IEEE J. Sel. Areas Commun. (2009)","DOI":"10.1109\/JSAC.2009.090408"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/MNET.2003.1248660","volume":"17","author":"J Gottlieb","year":"2003","unstructured":"Gottlieb, J., Greenberg, A., Rexford, J., Wang, J.: Automated provisioning of BGP customers. IEEE Netw. 17, 44\u201355 (2003)","journal-title":"IEEE Netw."},{"key":"14_CR12","unstructured":"Alaettinoglu, C., Villamizar, C., Gerich, E., Kessens, D., Meyer, D., Bates, T., Karrenberg, D., Terpstra, M.: Routing Policy Specification Language. RFC 2622"},{"key":"14_CR13","unstructured":"Bjorklund, M.: YANG - A Data Modeling Language for the Network Configuration Protocol (NETCONF). RFC 6020"},{"key":"14_CR14","unstructured":"Enns, R., et al.: Network Configuration Protocol (NETCONF). RFC 4741"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.: SDNRacer: concurrency analysis for SDNs. In: PLDI (2016)","DOI":"10.1145\/2908080.2908124"},{"key":"14_CR16","unstructured":"Canini, M., Venzano, D., Peresini, P., Kostic, D., Rexford, J., et al.: A NICE way to test OpenFlow applications. In: NSDI (2012)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Scott, C., Wundsam, A., Raghavan, B., Panda, A., Or, A., Lai, J., Huang, E., Liu, Z., El-Hassany, A., Whitlock, S., Acharya, H.B., Zarifis, K., Shenker, S.: Troubleshooting Blackbox SDN control software with minimal causal sequences. In: ACM SIGCOMM (2014)","DOI":"10.1145\/2619239.2626304"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"14_CR19","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":"14_CR20","doi-asserted-by":"crossref","unstructured":"Kang, N., Liu, Z., Rexford, J., Walker, D.: Optimizing the \u201cOne Big Switch\u201d abstraction in software-defined networks. In: CoNEXT (2013)","DOI":"10.1145\/2535372.2535373"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Benson, T., Akella, A., Maltz, D.A.: Mining policies from enterprise network configuration. In: IMC (2009)","DOI":"10.1145\/1644893.1644909"},{"key":"14_CR22","unstructured":"Awduche, D., et al.: Overview and Principles of Internet Traffic Engineering. RFC3272"},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1109\/MCOM.2002.1039866","volume":"40","author":"B Fortz","year":"2002","unstructured":"Fortz, B., Rexford, J., Thorup, M.: Traffic engineering with traditional IP routing protocols. IEEE Commun. Mag. 40, 118\u2013124 (2002)","journal-title":"IEEE Commun. Mag."},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1145\/502102.502104","volume":"48","author":"AY Halevy","year":"2001","unstructured":"Halevy, A.Y., Mumick, I.S., Sagiv, Y., Shmueli, O.: Static analysis in datalog extensions. J. ACM 48, 971\u20131012 (2001)","journal-title":"J. ACM"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF01536403","volume":"15","author":"IS Mumick","year":"1995","unstructured":"Mumick, I.S., Shmueli, O.: How expressive is stratified aggregation? Ann. Math. Artif. Intell. 15, 407\u2013435 (1995)","journal-title":"Ann. Math. Artif. Intell."},{"key":"14_CR26","unstructured":"El-Hassany, A., Tsankov, P., Vanbever, L., Vechev, M.T.: Network-wide configuration synthesis. CoRR, abs\/1611.02537 (2016). http:\/\/arxiv.org\/abs\/1611.02537"},{"key":"14_CR27","unstructured":"Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level (1995)"},{"key":"14_CR28","volume-title":"Principles of Database and Knowledge-Base Systems","author":"JD Ullman","year":"1989","unstructured":"Ullman, J.D.: Principles of Database and Knowledge-Base Systems. Computer Science Press, New York (1989)"},{"key":"14_CR29","unstructured":"https:\/\/logicblox.com\/content\/docs4\/corereference\/html\/index.html"},{"key":"14_CR30","unstructured":"Barrett, C., et al.: The SMT-LIB Standard: Version 2.0 (2010)"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR32","unstructured":"Graphical Network Simulator-3 (GNS3). https:\/\/www.gns3.com\/"},{"key":"14_CR33","doi-asserted-by":"publisher","first-page":"1765","DOI":"10.1109\/JSAC.2011.111002","volume":"29","author":"S Knight","year":"2011","unstructured":"Knight, S., Nguyen, H.X., Falkner, N., Bowden, R.A., Roughan, M.: The internet topology zoo. IEEE J. Sel. Areas Commun. 29, 1765\u20131775 (2011)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"14_CR34","volume-title":"Routing TCP\/IP","author":"J Doyle","year":"2005","unstructured":"Doyle, J., Carroll, J.: Routing TCP\/IP, vol. 1. Cisco Press, Indianapolis (2005)"},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-24206-9_14","volume-title":"Datalog Reloaded","author":"Y Smaragdakis","year":"2011","unstructured":"Smaragdakis, Y., Bravenboer, M.: Using datalog for fast and easy program analysis. In: de Moor, O., Gottlob, G., Furche, T., Sellers, A. (eds.) Datalog Reloaded. LNCS, vol. 6702, pp. 245\u2013251. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-24206-9_14"},{"key":"14_CR36","doi-asserted-by":"crossref","unstructured":"Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in datalog. In: PLDI (2014)","DOI":"10.1145\/2594291.2594327"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Madsen, M., Yee, M.-H., Lhot\u00e1k, O.: From datalog to flix: a declarative language for fixed points on lattices. In: PLDI (2016)","DOI":"10.1145\/2908080.2908096"},{"key":"14_CR38","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N., De Moura, L.: $$\\mu Z$$: an efficient engine for fixed points with constraints. In: CAV (2011)","DOI":"10.1007\/978-3-642-22110-1_36"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: EMSOFT (2006)","DOI":"10.1145\/1176887.1176896"},{"key":"14_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-68855-6_1","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"EK Jackson","year":"2008","unstructured":"Jackson, E.K., Schulte, W.: Model generation for horn logic with stratified negation. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 1\u201320. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-68855-6_1"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Jackson, E.K. Kang, E., Dahlweid, M., Seifert, D., Santen, T.: Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT (2010)","DOI":"10.1145\/1879021.1879027"},{"key":"14_CR42","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"26","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 26, 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"14_CR43","series-title":"TACAS 2014","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. TACAS 2014, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_26"},{"key":"14_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24730-2_15"},{"key":"14_CR45","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial Sketching for Finite Programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"14_CR46","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":"14_CR47","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10922-008-9108-y","volume":"16","author":"S Narain","year":"2008","unstructured":"Narain, S., Levin, G., Malik, S., Kaul, V.: Declarative infrastructure configuration synthesis and debugging. J. Netw. Syst. Manag. 16, 235\u2013258 (2008)","journal-title":"J. Netw. Syst. Manag."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:10:23Z","timestamp":1626135023000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}