{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T14:30:53Z","timestamp":1740148253794,"version":"3.37.3"},"reference-count":48,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2017,12,1]],"date-time":"2017-12-01T00:00:00Z","timestamp":1512086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Netw. Serv. Manage."],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1109\/tnsm.2017.2723725","type":"journal-article","created":{"date-parts":[[2017,7,5]],"date-time":"2017-07-05T18:04:45Z","timestamp":1499277885000},"page":"1113-1127","source":"Crossref","is-referenced-by-count":2,"title":["An Efficient Framework for Data-Plane Verification With Geometric Windowing Queries"],"prefix":"10.1109","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1411-8010","authenticated-orcid":false,"given":"Takeru","family":"Inoue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8073-3623","authenticated-orcid":false,"given":"Toru","family":"Mano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kimihiro","family":"Mizutani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hisashi","family":"Nagata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osamu","family":"Akashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/NETSOFT.2016.7502488"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77974-2_5"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1990.129849"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref30","first-page":"202","article-title":"Binary decision diagrams","volume":"4a","author":"knuth","year":"2011","journal-title":"The art of computer programming"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_4"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2716281.2836095"},{"key":"ref35","first-page":"533","article-title":"Enforcing network-wide policies in the presence of dynamic middlebox actions using FlowTags","author":"fayazbakhsh","year":"2014","journal-title":"Proc USENIX NSDI"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0352-z"},{"key":"ref10","first-page":"99","article-title":"Real time network policy checking using header space analysis","author":"kazemian","year":"2013","journal-title":"Proc USENIX NSDI"},{"key":"ref40","first-page":"127","article-title":"A NICE way to test OpenFlow applications","author":"canini","year":"2012","journal-title":"Proc USENIX NSDI"},{"key":"ref11","first-page":"15","article-title":"VeriFlow: Verifying network-wide invariants in real time","author":"khurshid","year":"2013","journal-title":"Proc USENIX NSDI"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"ref14","first-page":"499","article-title":"Checking beliefs in dynamic networks","author":"lopes","year":"2015","journal-title":"Proc USENIX NSDI"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2012.6364863"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2010.15"},{"key":"ref17","first-page":"101","article-title":"Software dataplane verification","author":"dobrescu","year":"2014","journal-title":"Proc USENIX NSDI"},{"key":"ref18","first-page":"469","article-title":"A general approach to network configuration analysis","author":"fogel","year":"2015","journal-title":"Proc USENIX NSDI"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837657"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/223\/03131"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2535372.2535376"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1544012.1544034"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1644893.1644909"},{"article-title":"A survey on network troubleshooting","year":"2012","author":"zeng","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77974-2_10"},{"key":"ref5","first-page":"1","article-title":"Why do Internet services fail, and what can be done about it?","author":"oppenheimer","year":"2003","journal-title":"Proc USENIX USITS"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2016.12.006"},{"key":"ref7","article-title":"Making SDNs work","author":"mckeown","year":"2012","journal-title":"Proc Open Netw Summit"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/SDN4FNS.2013.6702557"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2016.7784412"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/285237.285283"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342427"},{"key":"ref45","first-page":"209","article-title":"New directions for network verification","author":"panda","year":"2015","journal-title":"Proc SNAPL"},{"article-title":"Scalable verification of networks with packet transformers using atomic predicates","year":"2015","author":"yang","key":"ref48"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413205"},{"key":"ref47","first-page":"207","article-title":"Compiling path queries","author":"narayana","year":"2016","journal-title":"Proc USENIX NSDI"},{"key":"ref21","first-page":"73","article-title":"Enforcing generalized consistency properties in software-defined networks","author":"zhou","year":"2015","journal-title":"Proc USENIX NSDI"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"ref24","first-page":"113","article-title":"Header space analysis: Static checking for networks","author":"kazemian","year":"2012","journal-title":"Proc USENIX NSDI"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/EWSDN.2012.21"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"ref44","first-page":"386","article-title":"Temporal NetKAT","author":"beckett","year":"2015","journal-title":"Proc PLVNET"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413187"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/APNOMS.2014.6996558"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2014.52"}],"container-title":["IEEE Transactions on Network and Service Management"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/4275028\/8170467\/07968505.pdf?arnumber=7968505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:25:07Z","timestamp":1642004707000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7968505\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12]]},"references-count":48,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tnsm.2017.2723725","relation":{},"ISSN":["1932-4537"],"issn-type":[{"type":"print","value":"1932-4537"}],"subject":[],"published":{"date-parts":[[2017,12]]}}}