{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:07:21Z","timestamp":1773950841324,"version":"3.50.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T00:00:00Z","timestamp":1546819200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T00:00:00Z","timestamp":1546819200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007601","name":"Horizon 2020","doi-asserted-by":"publisher","award":["759102-SVIS"],"award-info":[{"award-number":["759102-SVIS"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011643","name":"Blavatnik Family Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100011643","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Blavatnik Interdisciplinary Cyber Research Center"},{"DOI":"10.13039\/501100009327","name":"PAZY Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100009327","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006221","name":"United States - Israel Binational Science Foundation","doi-asserted-by":"publisher","award":["2016260"],"award-info":[{"award-number":["2016260"]}],"id":[{"id":"10.13039\/100006221","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006221","name":"United States - Israel Binational Science Foundation","doi-asserted-by":"publisher","award":["2012259"],"award-info":[{"award-number":["2012259"]}],"id":[{"id":"10.13039\/100006221","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1704941"],"award-info":[{"award-number":["1704941"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1420064"],"award-info":[{"award-number":["1420064"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10703-018-00330-9","type":"journal-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T21:59:43Z","timestamp":1546984783000},"page":"191-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Some complexity results for stateful network verification"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6979-8880","authenticated-orcid":false,"given":"Kalev","family":"Alpernas","sequence":"first","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"}]},{"given":"Yaron","family":"Velner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,7]]},"reference":[{"key":"330_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla P, Jonsson B (1993) Verifying programs with unreliable channels. In: Logic in computer science (LICS). IEEE, pp 160\u2013170","DOI":"10.1109\/LICS.1993.287591"},{"key":"330_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla PA, \u010cer\u0101ns K, Jonsson B, Tsay YK (1996) General decidability theorems for infinite-state systems. In: Logic in computer science (LICS). IEEE, pp 313\u2013321","DOI":"10.1109\/LICS.1996.561359"},{"key":"330_CR3","unstructured":"Anderson CJ, Foster N, Guha A, Jeannin JB, Kozen D, Schlesinger C, Walker D (2014) NetKAT: semantic foundations for networks. In: POPL"},{"key":"330_CR4","doi-asserted-by":"crossref","unstructured":"Aref M, ten Cate B, Green TJ, Kimelfeld B, Olteanu D, Pasalic E, Veldhuizen TL, Washburn G (2015) Design and implementation of the LogicBlox system. In: ACM SIGMOD international conference on management of data, pp 1371\u20131382","DOI":"10.1145\/2723372.2742796"},{"key":"330_CR5","doi-asserted-by":"crossref","unstructured":"Ball T, Bj\u00f8rner N, Gember A, Itzhaky S, Karbyshev A, Sagiv M, Schapira M, Valadarsky A (2014) Vericon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN conference on programming language design and implementation, PLDI, p 31","DOI":"10.1145\/2666356.2594317"},{"issue":"4","key":"330_CR6","first-page":"361","volume":"2","author":"GV Bochmann","year":"1978","unstructured":"Bochmann GV (1978) Finite state description of communication protocols. Comput Netw 2(4):361\u2013372 (1976)","journal-title":"Comput Netw"},{"issue":"2","key":"330_CR7","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand D, Zafiropulo P (1983) On communicating finite-state machines. J ACM 30(2):323\u2013342","journal-title":"J ACM"},{"key":"330_CR8","unstructured":"Canini M, Venzano D, Peres P, Kostic D, Rexford J (2012) A nice way to test openflow applications. In: 9th USENIX symposium on networked systems design and implementation (NSDI\u201912)"},{"key":"330_CR9","doi-asserted-by":"crossref","unstructured":"Cardoza E, Lipton R, Meyer AR (1976) Exponential space complete problems for Petri nets and commutative semigroups (preliminary report). In: Proceedings of the eighth annual ACM symposium on theory of computing. ACM, pp 50\u201354","DOI":"10.1145\/800113.803630"},{"key":"330_CR10","unstructured":"Clarke EM, Jha S, Marrero WR (1998) Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: IFIP TC2\/WG2.2,2.3 international conference on programming concepts and methods (PROCOMET \u201998), Shelter Island, New York, USA, 8\u201312 June 1998, pp 87\u2013106"},{"issue":"1","key":"330_CR11","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 (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1):63\u201392","journal-title":"Theor Comput Sci"},{"key":"330_CR12","unstructured":"Fogel A, Fung S, Pedrosa L, Walraed-Sullivan M, Govindan R, Mahajan R, Millstein TD (2015) A general approach to network configuration analysis. In: 12th USENIX symposium on networked systems design and implementation, NSDI 15, Oakland, CA, USA, 4\u20136 May 2015, pp 469\u2013483"},{"key":"330_CR13","doi-asserted-by":"crossref","unstructured":"Foster N, Kozen D, Milano M, Silva A, Thompson L (2015) 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 Jan 2015, pp 343\u2013355","DOI":"10.1145\/2676726.2677011"},{"key":"330_CR14","doi-asserted-by":"crossref","unstructured":"Hengartner U, Moon S, Mortier R, Diot C (2002) Detection and analysis of routing loops in packet traces. In: Proceedings of the 2nd ACM SIGCOMM workshop on internet measurement. ACM, pp 107\u2013112","DOI":"10.1145\/637201.637217"},{"issue":"1","key":"330_CR15","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"s3-2","author":"Graham Higman","year":"1952","unstructured":"Higman G (1952) Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society, pp 326\u2013336","journal-title":"Proceedings of the London Mathematical Society"},{"key":"330_CR16","unstructured":"Kazemian P, Chang M, Zeng H, Varghese G, McKeown N, Whyte S (2013) Real time network policy checking using header space analysis. In: 10th USENIX symposium on networked systems design and implementation (NSDI \u201913)"},{"key":"330_CR17","unstructured":"Kazemian P, Varghese G, McKeown N (2012) Header space analysis: static checking for networks. In: 9th USENIX symposium on networked systems design and implementation (NSDI \u201912)"},{"issue":"4","key":"330_CR18","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 (2012) Veriflow: verifying network-wide invariants in real time. Comput Commun Rev 42(4):467\u2013472","journal-title":"Comput Commun Rev"},{"key":"330_CR19","doi-asserted-by":"crossref","unstructured":"Kozen D (1977) Lower bounds for natural proof systems. In: 18th annual symposium on foundations of computer science. IEEE, pp 254\u2013266","DOI":"10.1109\/SFCS.1977.16"},{"key":"330_CR20","doi-asserted-by":"crossref","unstructured":"Kuzniar M, Peresini P, Canini M, Venzano D, Kostic D (2012) A soft way for OpenFlow switch interoperability testing. In: CoNEXT, pp 265\u2013276","DOI":"10.1145\/2413176.2413207"},{"key":"330_CR21","unstructured":"Lipton R (1976) The reachability problem requires exponential space. Technical report 62, Department of Computer Science, Yale University"},{"key":"330_CR22","unstructured":"LogicBlox. \nhttp:\/\/www.logicblox.com\/\n\n. Retrieved 7 July 2015"},{"key":"330_CR23","unstructured":"Lola 2.0 sources. \nhttp:\/\/download.gna.org\/service-tech\/lola\/lola-2.0.tar.gz"},{"key":"330_CR24","unstructured":"Lopes NP, Bj\u00f8rner N, Godefroid P, Jayaraman K, Varghese G (2015) Checking beliefs in dynamic networks. In: 12th USENIX symposium on networked systems design and implementation, NSDI 15, Oakland, CA, USA, 4\u20136 May 2015, pp 499\u2013512"},{"key":"330_CR25","doi-asserted-by":"crossref","unstructured":"Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey B, King ST (2011) Debugging the data plane with anteater. In: SIGCOMM","DOI":"10.1145\/2018436.2018470"},{"key":"330_CR26","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"ML Minsky","year":"1961","unstructured":"Minsky ML (1961) Recursive unsolvability of post\u2019s problem of \u201ctag\u201d and other topics in theory of turing machines. Ann Math 74:437\u2013455","journal-title":"Ann Math"},{"key":"330_CR27","unstructured":"Nelson T, Ferguson AD, Scheer MJG, Krishnamurthi S (2014) 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 Apr 2014, pp 519\u2013531"},{"key":"330_CR28","unstructured":"Panda A, Argyraki KJ, Sagiv M, Schapira M, Shenker S (2015) New directions for network verification. In: 1st summit on advances in programming languages, SNAPL 2015, Asilomar, California, USA, 3\u20136 May 2015, pp 209\u2013220"},{"key":"330_CR29","unstructured":"Panda A, Lahav O, Argyraki K, Sagiv M, Shenker S (2014) Verifying isolation properties in the presence of middleboxes. arXiv preprint \narXiv:1409.7687"},{"issue":"3","key":"330_CR30","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"JL Peterson","year":"1977","unstructured":"Peterson JL (1977) Petri nets. ACM Comput Surv 9(3):223\u2013252","journal-title":"ACM Comput Surv"},{"key":"330_CR31","doi-asserted-by":"crossref","unstructured":"Potharaju R, Jain N (2013) 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 Oct 2013, pp 9\u201322","DOI":"10.1145\/2504730.2504737"},{"issue":"2","key":"330_CR32","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 (1978) The covering and boundedness problems for vector addition systems. Theor Comput Sci 6(2):223\u2013231","journal-title":"Theor Comput Sci"},{"key":"330_CR33","unstructured":"Ritchey RW, Ammann P (2000) Using model checking to analyze network vulnerabilities. In: Security and privacy"},{"key":"330_CR34","doi-asserted-by":"crossref","unstructured":"Schmidt K (2000) Lola a low level analyser. In: Application and theory of Petri nets 2000. Springer, pp 465\u2013474","DOI":"10.1007\/3-540-44988-4_27"},{"issue":"5","key":"330_CR35","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 (2002) Verifying lossy channel systems has nonprimitive recursive complexity. Inf Process Lett 83(5):251\u2013261","journal-title":"Inf Process Lett"},{"key":"330_CR36","doi-asserted-by":"crossref","unstructured":"Sen K, Viswanathan M (2006) Model checking multithreaded programs with asynchronous atomic methods. In: International conference on computer aided verification. Springer, pp 300\u2013314","DOI":"10.1007\/11817963_29"},{"key":"330_CR37","doi-asserted-by":"crossref","unstructured":"Sethi D, Narayana S, Malik S (2013) Abstractions for model checking SDN controllers. In: FMCAD","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"330_CR38","doi-asserted-by":"crossref","unstructured":"Sherry J, Hasan S, Scott C, Krishnamurthy A, Ratnasamy S, Sekar V (2012) Making middleboxes someone else\u2019s problem: network processing as a cloud service. In: SIGCOMM","DOI":"10.1145\/2342356.2342359"},{"key":"330_CR39","doi-asserted-by":"crossref","unstructured":"Skowyra R, Lapets A, Bestavros A, Kfoury A (2013) A verification platform for SDN-enabled applications. In: HiCoNS","DOI":"10.1109\/IC2E.2014.72"},{"key":"330_CR40","doi-asserted-by":"crossref","unstructured":"Stoenescu R, Popovici M, Negreanu L, Raiciu C (2013) Symnet: static checking for stateful networks. In: Proceedings of the 2013 workshop on Hot topics in middleboxes and network function virtualization. ACM, pp 31\u201336","DOI":"10.1145\/2535828.2535835"},{"key":"330_CR41","doi-asserted-by":"crossref","unstructured":"Velner Y, Alpernas K, Panda A, Rabinovich A, Sagiv M, Shenker S, Shoham S (2016) Some complexity results for stateful network verification. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 811\u2013830","DOI":"10.1007\/978-3-662-49674-9_51"},{"key":"330_CR42","unstructured":"Zeng H, Zhang S, Ye F, Jeyakumar V, Ju M, Liu J, McKeown N, Vahdat A (2014) Libra: divide and conquer to verify forwarding tables in huge networks. In: NSDI"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00330-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-00330-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00330-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:47:49Z","timestamp":1589730469000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-00330-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,7]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["330"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-00330-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,7]]},"assertion":[{"value":"7 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}