{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:57:17Z","timestamp":1773615437402,"version":"3.50.1"},"reference-count":14,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T00:00:00Z","timestamp":1417392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2014,12]]},"DOI":"10.3103\/s0146411614070165","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T19:16:45Z","timestamp":1422645405000},"page":"398-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A formal model and verification problems for software defined networks"],"prefix":"10.3103","volume":"48","author":[{"given":"V. A.","family":"Zakharov","sequence":"first","affiliation":[]},{"given":"R. L.","family":"Smelyansky","sequence":"additional","affiliation":[]},{"given":"E. V.","family":"Chemeritsky","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2015,2,1]]},"reference":[{"key":"6341_CR1","unstructured":"Open Flow Switch Specification. Version 1.4.0, 2013. www.opennetworking.org"},{"issue":"2","key":"6341_CR2","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1109\/MCOM.2013.6461195","volume":"51","author":"H Kim","year":"2013","unstructured":"Kim, H. and Feamster, N., Improving network management with software defined networking, Commun. Mag. IEEE, 2013, vol. 51, no. 2, pp. 114\u2013119.","journal-title":"Commun. Mag. IEEE"},{"key":"6341_CR3","first-page":"123","volume-title":"Proc. 17th IEEE Int. Conf. on Network Protocols (ICNP\u201909), Princeton, USA","author":"E Al-Shaer","year":"2009","unstructured":"Al-Shaer, E., Marrero, W., El-Atawy, A., and El Badawi, K., Network configuration in a box: Toward end-to-end verification of network reachability and security, Proc. 17th IEEE Int. Conf. on Network Protocols (ICNP\u201909), Princeton, USA, 2009, pp. 123\u2013132."},{"key":"6341_CR4","first-page":"290","volume-title":"Proc. Assoc. for Compt. Mach. SIGCOMM Conf.","author":"H Mai","year":"2011","unstructured":"Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, R.B., and King, S.T., Debugging of the data plane with anteater, Proc. Assoc. for Compt. Mach. SIGCOMM Conf., 2011, pp. 290\u2013301."},{"key":"6341_CR5","volume-title":"Proc. 9th USENIX Symp. on Networked Systems Design and Implementation","author":"P Kazemian","year":"2012","unstructured":"Kazemian, P., Varghese, G., and McKeown, N., Header space analysis: Static checking for networks, Proc. 9th USENIX Symp. on Networked Systems Design and Implementation 2012."},{"key":"6341_CR6","first-page":"49","volume-title":"Proc. Int. Conf. \u201cHot Topics in Software Defined Networking\u201d (HotSDN)","author":"A Khurshid","year":"2012","unstructured":"Khurshid, A., Zhou, W., Caesar, M., and Godfrey, P.B., VeriFlow: Verifying network-wide invariants in real time, Proc. Int. Conf. \u201cHot Topics in Software Defined Networking\u201d (HotSDN), 2012, pp. 49\u201354."},{"key":"6341_CR7","first-page":"79","volume-title":"Proc. Int. Conf. \u201cHot Topics in Software Defined Networking\u201d(HotSDN)","author":"S Gutz","year":"2012","unstructured":"Gutz, S., Story, A., Schlesinger, C, and Foster, N., Splendid isolation: A slice abstraction for software defined networks, Proc. Int. Conf. \u201cHot Topics in Software Defined Networking\u201d(HotSDN), 2012, pp. 79\u201384."},{"key":"6341_CR8","doi-asserted-by":"crossref","unstructured":"Reitblatt, M., Foster, N., Rexford, J., and Walker, D., Consistent updates for software-defined networks: Change you can believe in!, HotNets, 2011, vol. 7.","DOI":"10.1145\/2070562.2070569"},{"key":"6341_CR9","first-page":"323","volume-title":"Proc. Assoc. for Compt. Mach. SIGCOMM Conf.","author":"M Reitblatt","year":"2012","unstructured":"Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., and Walker, D., Abstractions for network update, Proc. Assoc. for Compt. Mach. SIGCOMM Conf., 2012, pp. 323\u2013334."},{"key":"6341_CR10","volume-title":"Proc. Networked Systems Design and Implementation","author":"M Canini","year":"2012","unstructured":"Canini, M., Venzano, D., Peresini, P., Kostic, D., and Rexford, J., A NICE way to test Open Flow applications, Proc. Networked Systems Design and Implementation, 2012."},{"key":"6341_CR11","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1137\/0216051","volume":"16","author":"N Immerman","year":"1987","unstructured":"Immerman, N., Languages that capture complexity classes, SIAM J. Compt., 1987, vol. 16, pp. 760\u2013778.","journal-title":"SIAM J. Compt."},{"key":"6341_CR12","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-63166-6_29","volume":"1254","author":"N Immerman","year":"1997","unstructured":"Immerman, N. and Vardi, M., Model checking and transitive closure logic, Lect. Notes Compt. Sci., 1997, vol. 1254, pp. 291\u2013302.","journal-title":"Lect. Notes Compt. Sci."},{"key":"6341_CR13","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1093\/jigpal\/8.3.325","volume":"8","author":"N Alechina","year":"2000","unstructured":"Alechina, N. and Immerman, N., Reachability logic: efficient fragment of transitive closure logic, Logic J. IGPL, 2000, vol. 8, pp. 325\u2013337.","journal-title":"Logic J. IGPL"},{"key":"6341_CR14","first-page":"77","volume-title":"Acta Informatica","author":"Z Galil","year":"1976","unstructured":"Galil, Z., Hierarchies of complete problems, Acta Informatica, 1976, no. 6, pp. 77\u201388."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070165.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411614070165","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411614070165.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:59:54Z","timestamp":1773611994000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411614070165"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12]]},"references-count":14,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["6341"],"URL":"https:\/\/doi.org\/10.3103\/s0146411614070165","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12]]},"assertion":[{"value":"10 November 2013","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 February 2015","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}