{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T05:09:42Z","timestamp":1745989782346,"version":"3.37.3"},"reference-count":52,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"Zhejiang Provincial Key Research and Development Program","award":["2021C01032"],"award-info":[{"award-number":["2021C01032"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62293511","62273305"],"award-info":[{"award-number":["62293511","62273305"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["226-2024-00004"],"award-info":[{"award-number":["226-2024-00004"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100017940","name":"Zhejiang Provincial Natural Science Foundation","doi-asserted-by":"publisher","award":["LZ22F030010"],"award-info":[{"award-number":["LZ22F030010"]}],"id":[{"id":"10.13039\/100017940","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Alibaba Cloud Alibaba Innovative Research Project"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE\/ACM Trans. Networking"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1109\/tnet.2024.3469386","type":"journal-article","created":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T17:29:07Z","timestamp":1727976547000},"page":"5475-5490","source":"Crossref","is-referenced-by-count":1,"title":["LFVeri: Network Configuration Verification for Virtual Private Cloud Networks"],"prefix":"10.1109","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5523-1330","authenticated-orcid":false,"given":"Kun","family":"Wang","sequence":"first","affiliation":[{"name":"State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6816-6459","authenticated-orcid":false,"given":"Chengcheng","family":"Zhao","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8643-5383","authenticated-orcid":false,"given":"Jinpei","family":"Chu","sequence":"additional","affiliation":[{"name":"College of Information Engineering, Zhejiang University of Technology, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1320-553X","authenticated-orcid":false,"given":"Yiping","family":"Shi","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2502-8686","authenticated-orcid":false,"given":"Jianyuan","family":"Lu","sequence":"additional","affiliation":[{"name":"Alibaba Group, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5528","authenticated-orcid":false,"given":"Biao","family":"Lyu","sequence":"additional","affiliation":[{"name":"Alibaba Group, Hangzhou, China"}]},{"given":"Shunmin","family":"Zhu","sequence":"additional","affiliation":[{"name":"Alibaba Group, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4221-2162","authenticated-orcid":false,"given":"Peng","family":"Cheng","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, Zhejiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3155-3145","authenticated-orcid":false,"given":"Jiming","family":"Chen","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Industrial Control Technology, Zhejiang University, Hangzhou, Zhejiang, China"}]}],"member":"263","reference":[{"volume-title":"Mitigating Cloud Vulnerabilities","year":"2020","key":"ref1"},{"key":"ref2","first-page":"217","article-title":"Efficient network reachability analysis using a succinct control plane representation","volume-title":"Proc. USENIX Symp. Oper. Syst. Design Implement. (OSDI)","author":"Fayaz"},{"volume-title":"Cisco ASA: All-in-One Firewall, IPS, Anti-X, and VPN Adaptive Security Appliance","year":"2009","author":"Frahim","key":"ref3"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1165389.945456"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2018.2868050"},{"key":"ref6","first-page":"469","article-title":"A general approach to network configuration analysis","volume-title":"Proc. USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Fogel"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_14"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_39"},{"issue":"1","key":"ref9","first-page":"351","article-title":"Survey of network verification","volume":"34","author":"Fang","year":"2021","journal-title":"J. Softw."},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"ref12","first-page":"953","article-title":"Plankton: Scalable network configuration verification through model checking","volume-title":"Proc. 17th USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Prabhu"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281432"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2023.3234931"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2022.3180631"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2022.3214062"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14977-6_2"},{"key":"ref18","first-page":"1","article-title":"Automated analysis and debugging of network connectivity policies","volume":"1","author":"Jayaraman","year":"2014","journal-title":"Microsoft Res."},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/69.43410"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"ref22","first-page":"735","article-title":"Delta-Net: Real-time network verification using atoms","volume-title":"Proc. USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Horn"},{"key":"ref23","first-page":"99","article-title":"Real time network policy checking using header space analysis","volume-title":"Proc. USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Kazemian"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"ref26","first-page":"241","article-title":"APKeep: Realtime verification for real networks","volume-title":"Proc. 17th USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Zhang"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/NFV-SDN.2016.7919488"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"ref29","first-page":"181","article-title":"NetSMC: A custom symbolic model checker for stateful network verification","volume-title":"Proc. 17th USENIX Symp. Networked Syst. Design Implement. (NSDI)","author":"Yuan"},{"key":"ref30","first-page":"699","article-title":"Verifying reachability in networks with mutable datapaths","volume-title":"Proc. 14th USENIX Symp. Networked Syst. Design Implement.","author":"Panda"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/TNSM.2020.3045781"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604859"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2014.2371999"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"ref37","first-page":"113","article-title":"Header space analysis: Static checking for networks","volume-title":"Proc. NSDI","author":"Kazemian"},{"key":"ref38","first-page":"499","article-title":"Checking beliefs in dynamic networks","volume-title":"Proc. USENIX Symp. Netw. Syst. Design Implement. (NSDI)","author":"Lopes"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2019.8888144"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_14"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_23"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v29i1.9755"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.1999.749256"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472925"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_1"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"volume-title":"LFVeri","year":"2024","key":"ref51"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2022.3193698"}],"container-title":["IEEE\/ACM Transactions on Networking"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/90\/10807683\/10703850.pdf?arnumber=10703850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,20]],"date-time":"2024-12-20T06:48:40Z","timestamp":1734677320000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10703850\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":52,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tnet.2024.3469386","relation":{},"ISSN":["1063-6692","1558-2566"],"issn-type":[{"type":"print","value":"1063-6692"},{"type":"electronic","value":"1558-2566"}],"subject":[],"published":{"date-parts":[[2024,12]]}}}