{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:35Z","timestamp":1762459295091,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_25","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"395-413","source":"Crossref","is-referenced-by-count":6,"title":["Static Differential Program Analysis for Software-Defined Networks"],"prefix":"10.1007","author":[{"given":"Tim","family":"Nelson","sequence":"first","affiliation":[]},{"given":"Andrew D.","family":"Ferguson","sequence":"additional","affiliation":[]},{"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Al-Shaer, E., Al-Haj, S.: FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures. In: Workshop on Assurable and Usable Security Configuration (2010)","DOI":"10.1145\/1866898.1866905"},{"key":"25_CR3","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: Principles of Programming Languages (POPL) (2014)"},{"key":"25_CR4","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: Programming Language Design and Implementation (PLDI) (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Bernays, P., Sch\u00f6nfinkel, M.: Zum entscheidungsproblem der mathematischen Logik. Mathematische Annalen\u00a099, 342\u2013372 (1928)","journal-title":"Mathematische Annalen"},{"key":"25_CR6","unstructured":"Canini, M., Venzano, D., Pere\u0161\u00edni, P., Kosti\u0107, D., Rexford, J.: A NICE way to test OpenFlow applications. In: Networked Systems Design and Implementation (2012)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Casado, M., Freedman, M.J., Pettit, J., Luo, J., McKeown, N., Shenker, S.: Ethane: Taking Control of the Enterprise. In: Conference on Communications Architectures, Protocols and Applications (SIGCOMM) (2007)","DOI":"10.1145\/1282380.1282382"},{"key":"25_CR8","unstructured":"Chen, C., Jia, L., Zhou, W., Loo, B.T.: Proof-based verification of software defined networks. In: Open Networking Summit (2014)"},{"key":"25_CR9","series-title":"LNCS(LNAI)","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/11814771_51","volume-title":"Automated Reasoning","author":"D.J. Dougherty","year":"2006","unstructured":"Dougherty, D.J., Fisler, K., Adsul, B.: Specifying and reasoning about dynamic access-control policies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS(LNAI), vol.\u00a04130, pp. 632\u2013646. Springer, Heidelberg (2006)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: Principles of Programming Languages (POPL) (2015)","DOI":"10.1145\/2676726.2677011"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Gutz, S., Story, A., Schlesinger, C., Foster, N.: Splendid isolation: A slice abstraction for software-defined networks. In: Workshop on Hot Topics in Software Defined Networking (2012)","DOI":"10.1145\/2342441.2342458"},{"key":"25_CR12","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-38574-2_20","volume-title":"Automated Deduction \u2013 CADE-24","author":"C. Hawblitzel","year":"2013","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol.\u00a07898, pp. 282\u2013299. Springer, Heidelberg (2013)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Horwitz, S.: Identifying the semantic and textual differences between two versions of a program. In: Programming Language Design and Implementation (PLDI) (1990)","DOI":"10.1145\/93542.93574"},{"key":"25_CR14","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press (2012)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Jain, S., Kumar, A., Mandal, S., Ong, J., Poutievski, L., Singh, A., Venkata, S., Wanderer, J., Zhou, J., Zhu, M., Zolla, J., H\u00f6lzle, U., Stuart, S., Vahdat, A.: B4: Experience with a globally-deployed software defined WAN. In: Conference on Communications Architectures, Protocols and Applications (SIGCOMM) (2013)","DOI":"10.1145\/2486001.2486019"},{"key":"25_CR16","unstructured":"Katta, N.P., Rexford, J., Walker, D.: Logic programming for software-defined networks. In: Workshop on Cross-Model Design and Validation (XLDI) (2012)"},{"key":"25_CR17","unstructured":"Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: Networked Systems Design and Implementation (2013)"},{"key":"25_CR18","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: Static checking for networks. In: Networked Systems Design and Implementation (2012)"},{"key":"25_CR19","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: Networked Systems Design and Implementation (2013)","DOI":"10.1145\/2342441.2342452"},{"key":"25_CR20","unstructured":"Koponen, T., Amidon, K., Balland, P., Casado, M., Chanda, A., Fulton, B., Ganichev, I., Gross, J., Gude, N., Ingram, P., Jackson, E., Lambeth, A., Lenglet, R., Li, S.H., Padmanabhan, A., Pettit, J., Pfaff, B., Ramanathan, R., Shenker, S., Shieh, A., Stribling, J., Thakkar, P., Wendlandt, D., Yip, A., Zhang, R.: Network Virtualization in Multi-tenant Datacenters. In: Networked Systems Design and Implementation (2014)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Foundations of Software Engineering (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-540-74835-9_11","volume-title":"Computer Security \u2013 ESORICS 2007","author":"A.X. Liu","year":"2007","unstructured":"Liu, A.X.: Change-impact analysis of firewall policies. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 155\u2013170. Springer, Heidelberg (2007)"},{"key":"25_CR24","unstructured":"Lopes, N., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., Varghese, G.: DNA pairing: Using differential network analysis to find reachability bugs. Tech. Rep. MSR-TR-2014-58, Microsoft Research (April 2014)"},{"key":"25_CR25","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: Conference on Communications Architectures, Protocols and Applications (SIGCOMM) (2011)","DOI":"10.1145\/2018436.2018470"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: Principles of Programming Languages (POPL) (2012)","DOI":"10.1145\/2103656.2103685"},{"key":"25_CR27","unstructured":"Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: Networked Systems Design and Implementation (2014)"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: Principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"25_CR29","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-30885-7_10","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"T. Nelson","year":"2012","unstructured":"Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Toward a more complete Alloy. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 136\u2013149. Springer, Heidelberg (2012)"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S.G., Pasareanu, C.S.: Differential symbolic execution. In: Foundations of Software Engineering (2008)","DOI":"10.1145\/1453101.1453131"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Porras, P., Shin, S., Yegneswaran, V., Fong, M., Tyson, M., Gu, G.: A security enforcement kernel for OpenFlow networks. In: Workshop on Hot Topics in Software Defined Networking (2012)","DOI":"10.1145\/2342441.2342466"},{"key":"25_CR33","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem in formal logic. Proceedings of the London Mathematical Society\u00a030, 264\u2013286 (1930)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Skowyra, R., Lapets, A., Bestavros, A., Kfoury, A.: A verification platform for SDN-enabled applications. In: International Conference on Cloud Engineering (2014)","DOI":"10.1109\/IC2E.2014.72"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-319-03545-1_3","volume-title":"Certified Programs and Proofs","author":"G. Stewart","year":"2013","unstructured":"Stewart, G.: Computational verification of network programs in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol.\u00a08307, pp. 33\u201349. Springer, Heidelberg (2013)"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Tariq, M.M.B., Bhandankar, K., Valancius, V., Zeitoun, A., Feamster, N., Ammar, M.H.: Answering \u201cwhat-if\u201d deployment and configuration questions with WISE: Techniques and deployment experience. IEEE\/ACM Transactions on Networking (February 2013)","DOI":"10.1109\/TNET.2012.2230448"},{"key":"25_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"25_CR38","unstructured":"Xie, G.G., Zhan, J., Maltz, D.A., Zhang, H., Greenberg, A., Hjalmtysson, G., Rexford, J.: On static reachability analysis of IP networks. In: IEEE Conference on Computer Communications (2005)"},{"key":"25_CR39","unstructured":"Zave, P., Rexford, J.: The design space of network mobility. In: Bonaventure, O., Haddadi, H. (eds.) Recent Advances in Networking. ACM SIGCOMM (2013)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:28:23Z","timestamp":1676942903000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}