{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:44:53Z","timestamp":1742928293229,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319686899"},{"type":"electronic","value":"9783319686905"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68690-5_28","type":"book-chapter","created":{"date-parts":[[2017,10,9]],"date-time":"2017-10-09T21:14:51Z","timestamp":1507583691000},"page":"464-480","source":"Crossref","is-referenced-by-count":0,"title":["An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics"],"prefix":"10.1007","author":[{"given":"Yuxin","family":"Deng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoqing","family":"Lei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,10,11]]},"reference":[{"key":"28_CR1","unstructured":"The Internet Topology Zoo Website. \nhttp:\/\/www.topology-zoo.org"},{"key":"28_CR2","unstructured":"The Maude Code. \nhttps:\/\/github.com\/zhmtechie\/NetKAT-Maude"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: Proceedings of the POPL 2014, pp. 113\u2013126. ACM (2014)","DOI":"10.1145\/2535838.2535862"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Beckett, R., Greenberg, M., Walker, D.: Temporal NetKAT. In: Proceedings of the PLDI 2016, pp. 386\u2013401. ACM (2016)","DOI":"10.1145\/2908080.2908108"},{"key":"28_CR5","series-title":"LNCS","volume-title":"All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Foster, N., Harrison, R., Freedman, M.J., Monsanto, C., Rexford, J., Story, A., Walker, D.: Frenetic: a network programming language. In: Proceedings of the ICFP 2011, pp. 279\u2013291. ACM (2011)","DOI":"10.1145\/2034773.2034812"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-49498-1_12","volume-title":"Programming Languages and Systems","author":"N Foster","year":"2016","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282\u2013309. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-662-49498-1_12"},{"key":"28_CR8","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 POPL 2015, pp. 343\u2013355. ACM (2015)","DOI":"10.1145\/2676726.2677011"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: Proceedings of the PLDI 2013, pp. 483\u2013494. ACM (2013)","DOI":"10.1145\/2491956.2462178"},{"issue":"3","key":"28_CR10","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: Proceedings of the POPL 2012, pp. 217\u2013230. ACM (2012)","DOI":"10.1145\/2103656.2103685"},{"key":"28_CR12","unstructured":"Monsanto, C., Reich, J., Foster, N., Rexford, J., Walker, D.: Composing software defined networks. In: Proceedings of the NSDI 2013, pp. 1\u201313. USENIX Association (2013)"},{"issue":"1\u20132","key":"28_CR13","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1016\/j.jlap.2005.09.008","volume":"67","author":"A Verdejo","year":"2006","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Executable structural operational semantics in Maude. J. Log. Algebr. Program. 67(1\u20132), 226\u2013293 (2006)","journal-title":"J. Log. Algebr. Program."},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-18378-2_19","volume-title":"Practical Aspects of Declarative Languages","author":"A Voellmy","year":"2011","unstructured":"Voellmy, A., Hudak, P.: Nettle: taking the sting out of programming network routers. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 235\u2013249. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-18378-2_19"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Voellmy, A., Wang, J., Yang, Y.R., Ford, B., Hudak, P.: Maple: simplifying SDN programming using algorithmic policies. In: Proceedings of the SIGCOMM 2013, pp. 87\u201398. ACM (2013)","DOI":"10.1145\/2486001.2486030"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68690-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T08:22:56Z","timestamp":1507796576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68690-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319686899","9783319686905"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68690-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}