{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:33Z","timestamp":1775868513576,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1111698, 1440744, 1413972, 1422046"],"award-info":[{"award-number":["1111698, 1440744, 1413972, 1422046"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-12-1-0757"],"award-info":[{"award-number":["N00014-12-1-0757"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,14]]},"DOI":"10.1145\/2676726.2677011","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"343-355","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["A Coalgebraic Decision Procedure for NetKAT"],"prefix":"10.1145","author":[{"given":"Nate","family":"Foster","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"given":"Mae","family":"Milano","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}]},{"given":"Laure","family":"Thompson","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2340820.2340823"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_3_2_2_5_1","volume-title":"Deciding Kleene algebras in Coq. Logical Methods in Computer Science, 8(1:16):1--42","author":"Braibant Thomas","year":"2012","unstructured":"Thomas Braibant and Damien Pous. Deciding Kleene algebras in Coq. Logical Methods in Computer Science, 8(1:16):1--42, 2012."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40164-0_10"},{"key":"e_1_3_2_2_7_1","volume-title":"NSDI","author":"Canini Marco","year":"2012","unstructured":"Marco Canini, Daniele Venzano, Peter Peres\u00edni, Dejan Kosti\u0107, and Jennifer Rexford. A NICE way to test OpenFlow applications. In NSDI, April 2012."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80634-0"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486003"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034812"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486019"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342435"},{"key":"e_1_3_2_2_16_1","volume-title":"NSDI","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian, George Varghese, and Nick McKeown. Header space analysis: Static checking for networks. In NSDI, April 2012."},{"key":"e_1_3_2_2_17_1","volume-title":"NSDI","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. VeriFlow: Verifying network-wide invariants in real time. In NSDI, April 2013."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_2_2_19_1","volume-title":"NSDI","author":"Koponen Teemu","year":"2014","unstructured":"Teemu Koponen, Keith Amidon, Peter Balland, Mart\u00edn Casado, Anupam Chanda, Bryan Fulton, Igor Ganichev, Jesse Gross, Natasha Gude, Paul Ingram, Ethan Jackson, Andrew Lambeth, Romain Lenglet, Shih-Hao Li, Amar Padmanabhan, Justin Pettit, Ben Pfaff, Rajiv Ramanathan, Scott Shenker, Alan Shieh, Jeremy Stribling, Pankaj Thakkar, Dan Wendlandt, Alexander Yip, and Ronghua Zhang. Network virtualization in multi-tenant datacenters. In NSDI, April 2014."},{"key":"e_1_3_2_2_20_1","first-page":"351","volume-title":"OSDI","author":"Koponen Teemu","year":"2010","unstructured":"Teemu Koponen, Martin Casado, Natasha Gude, Jeremy Stribling, Leon Poutievski, Min Zhu, Rajiv Ramanathan, Yuichiro Iwata, Hiroaki Inoue, Takayuki Hama, and Scott Shenker. Onix: A distributed control platform for large-scale production networks. In OSDI, pages 351--364, October 2010."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_2_24_1","first-page":"244","volume-title":"CSL","author":"Kozen Dexter","year":"1996","unstructured":"Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In CSL, pages 244--259, September 1996."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080126"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103685"},{"key":"e_1_3_2_2_27_1","volume-title":"NSDI","author":"Monsanto Christopher","year":"2013","unstructured":"Christopher Monsanto, Joshua Reich, Nate Foster, Jennifer Rexford, and David Walker. Composing software-defined networks. In NSDI, April 2013."},{"key":"e_1_3_2_2_28_1","volume-title":"NSDI","author":"Nelson Tim","year":"2014","unstructured":"Tim Nelson, Andrew D. Ferguson, Michael J. G. Scheer, and Shriram Krishnamurthi. Tierless programming and reasoning for software-defined networks. In NSDI, April 2014."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691453"},{"key":"e_1_3_2_2_30_1","volume-title":"February","author":"Pous Damien","year":"2013","unstructured":"Damien Pous. Relational algebra and KAT in Coq, February 2013. Available at http:\/\/perso.ens-lyon.fr\/damien.pous\/ra."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_3_2_2_32_1","first-page":"369","volume-title":"SOFSEM","author":"Rot Jurriaan","year":"2013","unstructured":"Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coalgebraic bisimulation-up-to. In SOFSEM, pages 369--381, January 2013."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701306"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626304"},{"key":"e_1_3_2_2_36_1","unstructured":"Alexandra Silva. Kleene Coalgebra. PhD thesis University of Nijmegen 2010."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2012.2.367"},{"issue":"1","key":"e_1_3_2_2_38_1","first-page":"9","volume":"9","author":"Silva Alexandra","year":"2013","unstructured":"Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Logical Methods in Computer Science, 9(1):9, 2013.","journal-title":"Rutten. Logical Methods in Computer Science"},{"key":"e_1_3_2_2_39_1","first-page":"235","volume-title":"PADL","author":"Voellmy Andreas","year":"2011","unstructured":"Andreas Voellmy and Paul Hudak. Nettle: Functional reactive programming of OpenFlow networks. In PADL, pages 235--249, January 2011."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486030"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413205"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2677011","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2677011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:56Z","timestamp":1750212716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2677011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":39,"alternative-id":["10.1145\/2676726.2677011","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2677011","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2677011","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}