{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:26:21Z","timestamp":1725909981237},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319675305"},{"type":"electronic","value":"9783319675312"}],"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-67531-2_10","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"155-171","source":"Crossref","is-referenced-by-count":2,"title":["Witnessing Network Transformations"],"prefix":"10.1007","author":[{"given":"Chaoqiang","family":"Deng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"10_CR1","unstructured":"ONOS: Open Network Operating System. \nhttp:\/\/onosproject.org\/"},{"key":"10_CR2","unstructured":"Open Daylight. \nhttps:\/\/www.opendaylight.org\/"},{"key":"10_CR3","unstructured":"RFC 6241 - Network Configuration Protocol (NETCONF). \nhttps:\/\/tools.ietf.org\/html\/rfc6241"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/503502.503503","volume":"23","author":"R Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273\u2013303 (2001). doi:\n10.1145\/503502.503503","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20\u201321, 2014, pp. 113\u2013126. ACM (2014). doi:\n10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"10_CR6","unstructured":"Canini, M., Venzano, D., Peres\u00edni, P., Kostic, D., Rexford, J.: A NICE way to test openflow applications. In: Gribble and Katabi [11], pp. 127\u2013140. \nhttps:\/\/www.usenix.org\/conference\/nsdi12\/technical-sessions\/presentation\/canini"},{"key":"10_CR7","unstructured":"Deng, C., Namjoshi, K.S.: Witnessing network transformations (2017). Extended version of this paper, at \nhttp:\/\/cs.nyu.edu\/~deng\/"},{"key":"10_CR8","unstructured":"Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Karp, R. (ed.) Complexity of Computation, SIAM-AMS Proc., pp. 27\u201341 (1974)"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2602204.2602219","volume":"44","author":"N Feamster","year":"2014","unstructured":"Feamster, N., Rexford, J., Zegura, E.W.: The road to SDN: an intellectual history of programmable networks. Comput. Commun. Rev. 44(2), 87\u201398 (2014). doi:\n10.1145\/2602204.2602219","journal-title":"Comput. Commun. Rev."},{"issue":"8","key":"10_CR10","doi-asserted-by":"publisher","first-page":"1698","DOI":"10.1016\/j.jcss.2015.06.004","volume":"81","author":"S Fortune","year":"2015","unstructured":"Fortune, S.: Equivalence and generalization in a layered network model. J. Comput. Syst. Sci. 81(8), 1698\u20131714 (2015). doi:\n10.1016\/j.jcss.2015.06.004","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR11","unstructured":"Gribble, S.D., Katabi, D. (eds.) Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, April 25\u201327, 2012. USENIX Association (2012). \nhttps:\/\/www.usenix.org\/publications\/proceedings\/?f[0]=im_group_audience%3A279"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16\u201319, 2013, pp. 483\u2013494. ACM (2013). doi:\n10.1145\/2462156.2462178","DOI":"10.1145\/2462156.2462178"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Kang, N., Liu, Z., Rexford, J., Walker, D.: Optimizing the \u201cone big switch\u201d abstraction in software-defined networks. In: Almeroth, K.C., Mathy, L., Papagiannaki, K., Misra, V. (eds.) Conference on emerging Networking Experiments and Technologies, CoNEXT 2013, Santa Barbara, CA, USA, December 9\u201312, 2013, pp. 13\u201324. ACM (2013). doi:\n10.1145\/2535372.2535373","DOI":"10.1145\/2535372.2535373"},{"key":"10_CR14","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: Gribble and Katabi[11], pp. 113\u2013126. \nhttps:\/\/www.usenix.org\/conference\/nsdi12\/technical-sessions\/presentation\/kazemian"},{"key":"10_CR15","unstructured":"Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: Veriflow: Verifying network-wide invariants in real time. In: Feamster, N., Mogul, J.C. (eds.) Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, April 2\u20135, 2013, pp. 15\u201327. USENIX Association (2013). \nhttps:\/\/www.usenix.org\/conference\/nsdi13\/technical-sessions\/presentation\/khurshid"},{"key":"10_CR16","unstructured":"Lopes, N.P., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4\u20136, 2015, pp. 499\u2013512. USENIX Association (2015). \nhttps:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/lopes"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, B., King, S.T.: Debugging the data plane with Anteater. In: Keshav, S., Liebeherr, J., Byers, J.W., Mogul, J.C. (eds.) Proceedings of the ACM SIGCOMM 2011 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Toronto, ON, Canada, August 15\u201319, 2011, pp. 290\u2013301. ACM (2011). doi:\n10.1145\/2018436.2018470","DOI":"10.1145\/2018436.2018470"},{"issue":"2","key":"10_CR18","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown, N., Anderson, T., Balakrishnan, H., Parulkar, G.M., Peterson, L.L., Rexford, J., Shenker, S., Turner, J.S.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69\u201374 (2008). doi:\n10.1145\/1355734.1355746","journal-title":"Comput. Commun. Rev."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38856-9_17"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI) 2000, pp. 83\u201395 (2000)","DOI":"10.1145\/349299.349314"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: OSDI (1996)","DOI":"10.1145\/238721.238781"},{"issue":"2","key":"10_CR22","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT) - automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192\u2013201 (1998)","journal-title":"Softw. Tools Technol. Transf."},{"key":"10_CR23","unstructured":"Rinard, M.C., Marinov, D.: Credible compilation with pointers. In: FLoC Workshop on Run-Time Result Verification (1999)"},{"key":"10_CR24","unstructured":"Shenker, S., Casado, M., Koponen, T., McKeown, N.: The future of networking and the past of protocols. Open Networking Summit (2011)"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Simsarian, J.E., Choi, N., Kim, Y.J., Fortune, S., Thottan, M.K.: Netgraph data model applied to multilayer carrier networks. In: OFC (2016). doi:\n10.1364\/OFC.2016.Th4G.2","DOI":"10.1364\/OFC.2016.Th4G.2"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for netkat. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1\u20133, 2015, pp. 328\u2013341. ACM (2015). doi:\n10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"issue":"3","key":"10_CR27","first-page":"223","volume":"9","author":"LD Zuck","year":"2003","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223\u2013247 (2003)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:36:17Z","timestamp":1504604177000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}