{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T22:17:26Z","timestamp":1755037046335},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319997247"},{"type":"electronic","value":"9783319997254"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_8","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T13:45:50Z","timestamp":1535550350000},"page":"86-106","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Abstract Interpretation of Stateful Networks"],"prefix":"10.1007","author":[{"given":"Kalev","family":"Alpernas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roman","family":"Manevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aurojit","family":"Panda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"Shenker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yaron","family":"Velner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alpernas, K., et al.: Abstract interpretation of stateful networks. arXiv preprint arXiv:1708.05904 (2018)","DOI":"10.1007\/978-3-319-99725-4_8"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL (2014)","DOI":"10.1145\/2535838.2535862"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Aref, M., et al.: Design and implementation of the LogicBlox system. In: ACM SIGMOD International Conference on Management of Data, pp. 1371\u20131382 (2015)","DOI":"10.1145\/2723372.2742796"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, p. 31 (2014)","DOI":"10.1145\/2666356.2594317"},{"key":"8_CR5","unstructured":"Canini, M., Venzano, D., Peres, P., Kostic, D., Rexford, J.: A NICE way to test OpenFlow applications. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012) (2012)"},{"key":"8_CR6","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-0-387-35358-6_10","volume-title":"Programming Concepts and Methods PROCOMET 1998","author":"EM Clarke","year":"1998","unstructured":"Clarke, E.M., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Gries, D., de Roever, W.-P. (eds.) Programming Concepts and Methods PROCOMET 1998. ITIFIP, pp. 87\u2013106. Springer, Boston, MA (1998). https:\/\/doi.org\/10.1007\/978-0-387-35358-6_10"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-39799-8_8","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124\u2013140. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_8"},{"key":"8_CR9","unstructured":"Fayaz, S.K., Yu, T., Tobioka, Y., Chaki, S., Sekar, V., Vyas, S.: BUZZ: testing context-dependent policies in stateful networks. In: NSDI (2016)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"issue":"1\u20133","key":"8_CR11","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci. 338(1\u20133), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 343\u2013355 (2015)","DOI":"10.1145\/2676726.2677011"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: POPL, pp. 473\u2013485 (2017)","DOI":"10.1145\/3009837.3009893"},{"key":"8_CR14","unstructured":"Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2013) (2013)"},{"key":"8_CR15","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012) (2012)"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1145\/2377677.2377766","volume":"42","author":"A Khurshid","year":"2012","unstructured":"Khurshid, A., Zhou, W., Caesar, M., Godfrey, B.: VeriFlow: verifying network-wide invariants in real time. Comput. Commun. Rev. 42(4), 467\u2013472 (2012)","journal-title":"Comput. Commun. Rev."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Kuzniar, M., Peresini, P., Canini, M., Venzano, D., Kostic, D.: A SOFT way for OpenFlow switch interoperability testing. In: CoNEXT, pp. 265\u2013276 (2012)","DOI":"10.1145\/2413176.2413207"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, B., King, S.T.: Debugging the data plane with anteater. In: SIGCOMM (2011)","DOI":"10.1145\/2018436.2018470"},{"key":"8_CR19","unstructured":"Marmorstein, R.M., Kearns, P.: A tool for automated iptables firewall analysis. In: USENIX Annual Technical Conference, Freenix Track, pp. 71\u201381 (2005)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Mayer, A., Wool, A., Ziskind, E.: Fang: a firewall analysis engine. In: Proceedings of 2000 IEEE Symposium on Security and Privacy, S&P 2000, pp. 177\u2013187. IEEE (2000)","DOI":"10.1109\/SECPRI.2000.848455"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-642-35873-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496\u2013514. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_29"},{"key":"8_CR22","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The margrave tool for firewall analysis. In: LISA (2010)"},{"key":"8_CR23","unstructured":"Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, 2\u20134 April 2014, pp. 519\u2013531 (2014)"},{"key":"8_CR24","unstructured":"Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying reachability in networks with mutable datapaths. In: 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017, Boston, MA, USA, 27\u201329 March 2017, pp. 699\u2013718 (2017)"},{"key":"8_CR25","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: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 69\u201383 (2016)","DOI":"10.1145\/2837614.2837657"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with $$(0,1, \\infty )$$(0,1,\u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107\u2013122. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_9"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Potharaju, R., Jain, N.: Demystifying the dark side of the middle: a field study of middlebox failures in datacenters. In: Proceedings of the 2013 Internet Measurement Conference, IMC 2013, Barcelona, Spain, 23\u201325 October 2013, pp. 9\u201322 (2013)","DOI":"10.1145\/2504730.2504737"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Ritchey, R.W., Ammann, P.: Using model checking to analyze network vulnerabilities. In: Security and Privacy (2000)","DOI":"10.1109\/SECPRI.2000.848453"},{"issue":"2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0304-3975(88)90049-7","volume":"60","author":"AW Roscoe","year":"1988","unstructured":"Roscoe, A.W., Hoare, C.A.R.: The laws of OCCAM programming. Theor. Comput. Sci. 60(2), 177\u2013229 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Sherry, J., Hasan, S., Scott, C., Krishnamurthy, A., Ratnasamy, S., Sekar, V.: Making middleboxes someone else\u2019s problem: network processing as a cloud service. In: SIGCOMM (2012)","DOI":"10.1145\/2342356.2342359"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Sivaraman, A., et al.: Packet transactions: high-level programming for line-rate switches. In: Proceedings of the ACM SIGCOMM 2016 Conference, Florianopolis, Brazil, 22\u201326 August 2016, pp. 15\u201328 (2016)","DOI":"10.1145\/2934872.2934900"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Skowyra, R., Lapets, A., Bestavros, A., Kfoury, A.: A verification platform for SDN-enabled applications. In: HiCoNS (2013)","DOI":"10.1109\/IC2E.2014.72"},{"key":"8_CR34","unstructured":"Stoenescu, R., Popovici, M., Negreanu, L., Raiciu, C.: Scalable symbolic execution for modern networks. In: SIGCOMM (2016)"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1007\/978-3-662-49674-9_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Velner","year":"2016","unstructured":"Velner, Y., et al.: Some complexity results for stateful network verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 811\u2013830. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_51"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T13:41:48Z","timestamp":1693834908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}