{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:07:17Z","timestamp":1773950837380,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_51","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"811-830","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Some Complexity Results for Stateful Network Verification"],"prefix":"10.1007","author":[{"given":"Yaron","family":"Velner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kalev","family":"Alpernas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aurojit","family":"Panda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Rabinovich","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"}]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"51_CR1","unstructured":"Lola 2.0 sources. http:\/\/download.gna.org\/service-tech\/lola\/lola-2.0.tar.gz"},{"key":"51_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. In: Logic in Computer Science (LICS), pp. 160\u2013170. IEEE (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"51_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Logic in Computer Science (LICS), pp. 313\u2013321. IEEE (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"51_CR4","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.-B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: POPL (2014)"},{"key":"51_CR5","doi-asserted-by":"crossref","unstructured":"Aref, M., ten Cate, B., Green, T.J., Kimelfeld, B., Olteanu, D., Pasalic, E., Veldhuizen, T.L., Washburn, G.: 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":"51_CR6","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: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, p. 31 (2014)","DOI":"10.1145\/2594291.2594317"},{"issue":"4\u20135","key":"51_CR7","first-page":"361","volume":"2","author":"GV Bochmann","year":"1978","unstructured":"Bochmann, G.V.: Finite state description of communication protocols. Comput. Netw. 2(4\u20135), 361\u2013372 (1978)","journal-title":"Comput. Netw."},{"issue":"2","key":"51_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM (JACM) 30(2), 323\u2013342 (1983)","journal-title":"J. ACM (JACM)"},{"key":"51_CR9","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":"51_CR10","doi-asserted-by":"crossref","unstructured":"Cardoza, E., Lipton, R., Meyer, A.R.: Exponential space complete problems for petri nets and commutative semigroups (preliminary report). In: Proceedings of the Eighth Annual ACM Symposium on Theory of Computing, pp. 50\u201354. ACM (1976)","DOI":"10.1145\/800113.803630"},{"key":"51_CR11","series-title":"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. IFIP, pp. 87\u2013106. Springer, Heidelberg (1998)"},{"issue":"1","key":"51_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theoret. Comput. Sci. 256(1), 63\u201392 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"51_CR13","unstructured":"Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., Millstein, T.D.: A general approach to network configuration analysis. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4\u20136, pp. 469\u2013483 (2015)"},{"key":"51_CR14","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 , Mumbai, India, 15\u201317 January 2015, pp. 343\u2013355 (2015)","DOI":"10.1145\/2676726.2677011"},{"key":"51_CR15","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":"51_CR16","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":"51_CR17","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":"51_CR18","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":"51_CR19","unstructured":"Lopes, N.P., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4\u20136, pp. 499\u2013512 (2015)"},{"key":"51_CR20","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":"51_CR21","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, Seattle, WA, USA, April 2\u20134, 2014, pp. 519\u2013531 (2014)"},{"key":"51_CR22","unstructured":"OpenStack. LogicBlox. http:\/\/www.logicblox.com\/ . Accessed 07 July 2015"},{"key":"51_CR23","unstructured":"Panda, A., Argyraki, K.J., Sagiv, M., Schapira, M., Shenker, S.: New directions for network verification. In: 1st Summit on Advances in Programming Languages, SNAPL 3\u20136, 2015, Asilomar, California, USA, pp. 209\u2013220, May 2015"},{"key":"51_CR24","unstructured":"Panda, A., Lahav, O., Argyraki, K., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes (2014). arXiv preprint arXiv: 1409.7687"},{"key":"51_CR25","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, October 23\u201325, 2013, pp. 9\u201322 (2013)"},{"issue":"2","key":"51_CR26","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoret. Comput. Sci. 6(2), 223\u2013231 (1978)","journal-title":"Theoret. Comput. Sci."},{"key":"51_CR27","unstructured":"Ritchey, R.W., Ammann, P.: Using model checking to analyze network vulnerabilities. In: Security and Privacy (2000)"},{"key":"51_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-44988-4_27","volume-title":"Application and Theory of Petri Nets 2000","author":"K Schmidt","year":"2000","unstructured":"Schmidt, K.: LoLA a low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 465. Springer, Heidelberg (2000)"},{"issue":"5","key":"51_CR29","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"P Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251\u2013261 (2002)","journal-title":"Inf. Process. Lett."},{"key":"51_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":"51_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":"51_CR32","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":"51_CR33","doi-asserted-by":"crossref","unstructured":"Stoenescu, R., Popovici, M., Negreanu, L., Raiciu, C.: Symnet: static checking for stateful networks. In: Proceedings of the 2013 Workshop on Hot Topics in Middleboxes and Network Function Virtualization, pp. 31\u201336. ACM (2013)","DOI":"10.1145\/2535828.2535835"},{"key":"51_CR34","unstructured":"Velner, Y., Aplernas, K., Panda, A., Rabinovich, A., Sagiv, M., Shenker, S., Shoham, S.: Some complexity results for stateful network verification. http:\/\/www.cs.tau.ac.il\/~msagiv\/tacas16submission.pdf"},{"key":"51_CR35","unstructured":"Zeng, H., Zhang, S., Ye, F., Jeyakumar, V., Ju, M., Liu, J., McKeown, N., Vahdat, A.: Libra: Divide and conquer to verify forwarding tables in huge networks. In: NSDI (2014)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:30:07Z","timestamp":1748853007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}