{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:14Z","timestamp":1772164034692,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,6,9]],"date-time":"2014-06-09T00:00:00Z","timestamp":1402272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Technical University of Munich"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,6,9]]},"DOI":"10.1145\/2594291.2594317","type":"proceedings-article","created":{"date-parts":[[2014,5,13]],"date-time":"2014-05-13T08:18:34Z","timestamp":1399969114000},"page":"282-293","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":71,"title":["VeriCon"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[{"name":"Microsoft Research"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[{"name":"Microsoft Research"}]},{"given":"Aaron","family":"Gember","sequence":"additional","affiliation":[{"name":"University of Madison-Wisconsin"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Tel Aviv University"}]},{"given":"Aleksandr","family":"Karbyshev","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University"}]},{"given":"Michael","family":"Schapira","sequence":"additional","affiliation":[{"name":"Hebrew University"}]},{"given":"Asaf","family":"Valadarsky","sequence":"additional","affiliation":[{"name":"Hebrew University"}]}],"member":"320","published-online":{"date-parts":[[2014,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"OpenFlow Switch Specification Oct. 2013. Version 1.4.0. OpenFlow Switch Specification Oct. 2013. Version 1.4.0."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_1_3_1","volume-title":"NSDI","author":"Canini M.","year":"2012","unstructured":"Canini , M. , Venzano , D. , Peres , P. , Kostic , D. , and Rexford , J . A NICE Way to Test OpenFlow Applications . In NSDI ( 2012 ). Canini, M., Venzano, D., Peres, P., Kostic, D., and Rexford, J. A NICE Way to Test OpenFlow Applications. In NSDI (2012)."},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"TACAS","author":"de Moura L. M.","year":"2008","unstructured":"de Moura , L. M. , and Bj\u00f8rner , N . Z3: An Efficient SMT Solver . In TACAS ( 2008 ), C. R. Ramakrishnan and J. Rehof, Eds ., vol. 4963 of Lecture Notes in Computer Science , Springer , pp. 337 -- 340 . de Moura, L. M., and Bj\u00f8rner, N. Z3: An Efficient SMT Solver. In TACAS (2008), C. R. Ramakrishnan and J. Rehof, Eds., vol. 4963 of Lecture Notes in Computer Science, Springer, pp. 337--340."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2013.6461197"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2011.02.002"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486019"},{"key":"e_1_3_2_1_12_1","volume-title":"ACM SIGPLAN Workshop on Cross-model Language Design and Implementation (Sept.","author":"Katta N. P.","year":"2012","unstructured":"Katta , N. P. , Rexford , J. , and Walker , D . Logic programming for software-defined networks . In ACM SIGPLAN Workshop on Cross-model Language Design and Implementation (Sept. 2012 ). Katta, N. P., Rexford, J., and Walker, D. Logic programming for software-defined networks. In ACM SIGPLAN Workshop on Cross-model Language Design and Implementation (Sept. 2012)."},{"key":"e_1_3_2_1_13_1","volume-title":"10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13)","author":"Kazemian P.","year":"2013","unstructured":"Kazemian , P. , Chang , M. , Zeng , H. , Varghese , G. , McKeown , N. , and Whyte , S . Real Time Network Policy Checking using Header Space Analysis . In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13) ( 2013 ). Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., and Whyte, S. Real Time Network Policy Checking using Header Space Analysis. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI '13) (2013)."},{"key":"e_1_3_2_1_14_1","volume-title":"N. Header Space Analysis: Static Checking For Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12)","author":"Kazemian P.","year":"2012","unstructured":"Kazemian , P. , Varghese , G. , and McKeown , N. Header Space Analysis: Static Checking For Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12) ( 2012 ). Kazemian, P., Varghese, G., and McKeown, N. Header Space Analysis: Static Checking For Networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI '12) (2012)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_2_1_16_1","volume-title":"11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14)","author":"Koponen T.","year":"2014","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. , and Zhang , R . Network virtualization in multi-tenant datacenters . In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14) ( 2014 ). 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., and Zhang, R. Network virtualization in multi-tenant datacenters. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14) (2014)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413207"},{"key":"e_1_3_2_1_18_1","first-page":"21","volume-title":"IFIP Congress","author":"McCarthy J.","year":"1962","unstructured":"McCarthy , J. Towards a mathematical science of computation . In IFIP Congress ( 1962 ), pp. 21 -- 28 . McCarthy, J. Towards a mathematical science of computation. In IFIP Congress (1962), pp. 21--28."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592681.1592684"},{"key":"e_1_3_2_1_20_1","volume-title":"11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14)","author":"Nelson T.","year":"2014","unstructured":"Nelson , T. , Ferguson , A. D. , Scheer , M. J. G. , and Krishnamurthi , S . A balance of power: Expressive, analyzable controller programming . In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14) ( 2014 ). Nelson, T., Ferguson, A. D., Scheer, M. J. G., and Krishnamurthi, S. A balance of power: Expressive, analyzable controller programming. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI '14) (2014)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486022"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342427"},{"key":"e_1_3_2_1_23_1","volume-title":"FMCAD","author":"Sethi D.","year":"2013","unstructured":"Sethi , D. , Narayana , S. , and Malik , S . Abstractions for model checking sdn controllers . In FMCAD ( 2013 ). Sethi, D., Narayana, S., and Malik, S. Abstractions for model checking sdn controllers. In FMCAD (2013)."},{"key":"e_1_3_2_1_24_1","volume-title":"HiCoNS","author":"Skowyra R.","year":"2013","unstructured":"Skowyra , R. , Lapets , A. , Bestavros , A. , and Kfoury , A . A verification platform for sdn-enabled applications . In HiCoNS ( 2013 ). Skowyra, R., Lapets, A., Bestavros, A., and Kfoury, A. A verification platform for sdn-enabled applications. In HiCoNS (2013)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486030"}],"event":{"name":"PLDI '14: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Edinburgh United Kingdom","acronym":"PLDI '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","NSF"]},"container-title":["Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2594291.2594317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:01:05Z","timestamp":1750215665000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594317"}},"subtitle":["towards verifying controller programs in software-defined networks"],"short-title":[],"issued":{"date-parts":[[2014,6,9]]},"references-count":24,"alternative-id":["10.1145\/2594291.2594317","10.1145\/2594291"],"URL":"https:\/\/doi.org\/10.1145\/2594291.2594317","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2666356.2594317","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,6,9]]},"assertion":[{"value":"2014-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}