{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:03:18Z","timestamp":1740099798686,"version":"3.37.3"},"reference-count":33,"publisher":"IEEE","license":[{"start":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T00:00:00Z","timestamp":1605571200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T00:00:00Z","timestamp":1605571200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T00:00:00Z","timestamp":1605571200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61802225"],"award-info":[{"award-number":["61802225"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,11,17]]},"DOI":"10.1109\/mascots50786.2020.9285941","type":"proceedings-article","created":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T23:22:16Z","timestamp":1608592936000},"page":"1-8","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Execution for Network Functions with Time-Driven Logic"],"prefix":"10.1109","author":[{"given":"Harsha","family":"Sharma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenfei","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bangwen","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3005745.3005755"},{"key":"ref32","first-page":"699","article-title":"Alembic: automated model inference for stateful network functions","author":"moon","year":"0","journal-title":"16th USENIX Symposium on Networked Systems Design and Implementation ( NSDI 19)"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2017.8057041"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3152434.3152439"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2008.4626228"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934892"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"ref13","first-page":"315","article-title":"VFP: A virtual switch platform for host SDN in the public cloud","author":"firestone","year":"2017","journal-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)"},{"journal-title":"Vaighese G Hashed and Hierarchical Timing Wheels Efficient Data Structures for Implementing A Timer Facility","year":"1996","author":"varghese","key":"ref14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3342280.3342344"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_40"},{"year":"0","key":"ref17"},{"key":"ref18","first-page":"337","article-title":"Z3: An efficient smt solver","author":"de moura","year":"0","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/354871.354874"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_8"},{"key":"ref4","first-page":"699","article-title":"Verifying reachability in networks with mutable datapaths","author":"panda","year":"2017","journal-title":"Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation ser NSDI’ 17"},{"journal-title":"Formally verifiable networking","year":"2009","author":"wang","key":"ref27"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"journal-title":"Tiramisu Fast and general network verification","year":"2019","author":"abhashkumar","key":"ref29"},{"key":"ref5","first-page":"275","article-title":"Buzz: Testing context-dependent policies in stateful networks","author":"fayaz","year":"2016","journal-title":"Proceedings of the 13th Usenix Conference on Networked Systems Design and Implementation ser NSDI'16"},{"key":"ref8","first-page":"209","article-title":"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation Ser OSDI'08"},{"key":"ref7","first-page":"101","article-title":"Software dataplane verification","author":"dobrescu","year":"2014","journal-title":"Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation ser NSDI'14"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"ref1","first-page":"9","article-title":"Header space analysis: Static checking for networks","author":"kazemian","year":"2012","journal-title":"Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation Ser NSDI'12"},{"key":"ref9","first-page":"59","article-title":"Kinetic: Verifiable dynamic network control","author":"kim","year":"0","journal-title":"12th USENIX Symposium on Networked Systems Design and Implementation ( NSDI 15)"},{"journal-title":"Appendix with nf models code","year":"0","key":"ref20"},{"key":"ref22","first-page":"153","author":"huang","year":"2019","journal-title":"Nfd Using behavior models to develop cross-platform nfs"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034812"},{"key":"ref24","first-page":"113","article-title":"Mos: A reusable networking stack for flow monitoring middleboxes","author":"jamshed","year":"0","journal-title":"14th USENIX Symposium on Networked Systems Design and Implementation NSDI 17)"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230562"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230563"}],"event":{"name":"2020 28th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS)","start":{"date-parts":[[2020,11,17]]},"location":"Nice, France","end":{"date-parts":[[2020,11,19]]}},"container-title":["2020 28th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9285930\/9285931\/09285941.pdf?arnumber=9285941","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,28]],"date-time":"2022-06-28T21:50:47Z","timestamp":1656453047000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9285941\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,17]]},"references-count":33,"URL":"https:\/\/doi.org\/10.1109\/mascots50786.2020.9285941","relation":{},"subject":[],"published":{"date-parts":[[2020,11,17]]}}}