{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T23:10:05Z","timestamp":1752275405807,"version":"3.41.2"},"reference-count":45,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T00:00:00Z","timestamp":1751328000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T00:00:00Z","timestamp":1751328000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T00:00:00Z","timestamp":1751328000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["2023SCU12128"],"award-info":[{"award-number":["2023SCU12128"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2025,7]]},"DOI":"10.1109\/tdsc.2025.3543437","type":"journal-article","created":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T14:11:02Z","timestamp":1739974262000},"page":"4200-4214","source":"Crossref","is-referenced-by-count":0,"title":["Fast Inverse Model Transformation: An Algebraic Framework for Fast Data Plane Verification"],"prefix":"10.1109","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0231-0638","authenticated-orcid":false,"given":"Shenshen","family":"Chen","sequence":"first","affiliation":[{"name":"School of Computer Science and Technology, Tongji University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4521-2125","authenticated-orcid":false,"given":"Jian","family":"Luo","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Engineering, Sichuan University, Chengdu, China"}]},{"given":"Dong","family":"Guo","sequence":"additional","affiliation":[{"name":"School of Computer Science, Fudan University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2037-4427","authenticated-orcid":false,"given":"Kai","family":"Gao","sequence":"additional","affiliation":[{"name":"School of Cyber Science and Engineering, Sichuan University, Chengdu, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7460-8164","authenticated-orcid":false,"given":"Yang Richard","family":"Yang","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Yale University, New Haven, CT, USA"}]}],"member":"263","reference":[{"article-title":"Amazon AWS outage","year":"2020","author":"Gumaste","key":"ref1"},{"article-title":"Prolonged AWS outage takes down a big chunk of the internet","year":"2020","author":"Peters","key":"ref2"},{"article-title":"Google suffers global outage with Gmail, YouTube and majority of services affected","year":"2020","author":"Hern","key":"ref3"},{"year":"2021","key":"ref4","article-title":"More details about the October 4 outage"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934909"},{"key":"ref6","first-page":"579","article-title":"NetComplete: Practical network-wide configuration synthesis with autocompletion","volume-title":"Proc. 15th USENIX Symp. Netw. Syst. Des. Implementation","author":"El-Hassany"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062367"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"ref9","first-page":"469","article-title":"A general approach to network configuration analysis","volume-title":"Proc. 12th USENIX Symp. Netw. Syst. Des. Implementation","author":"Fogel"},{"key":"ref10","first-page":"599","article-title":"Coverage: A practical configuration verifier on a global WAN","volume-title":"Proc. Annu. Conf. ACM Special Int. Group Data Commun. Appl. Technol. Architectures Protoc. Comput. Commun.","author":"Ye"},{"key":"ref11","first-page":"217","article-title":"Efficient network reachability analysis using a succinct control plane representation","volume-title":"Proc. 12th USENIX Symp. Operating Syst. Des. Implementation","author":"Seyed"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3371110"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132753"},{"article-title":"Tiramisu: Fast and general network verification","year":"2019","author":"Abhashkumar","key":"ref14"},{"key":"ref15","first-page":"953","article-title":"Plankton: Scalable network configuration verification through model checking","volume-title":"Proc. 17th USENIX Symp. Netw. Syst. Des. Implementation","author":"Prabhu"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1866898.1866905"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"ref19","first-page":"113","article-title":"Header space analysis: Static checking for networks","volume-title":"Proc. 9th USENIX Symp. Netw. Syst. Des. Implementation","author":"Kazemian"},{"key":"ref20","first-page":"87","article-title":"Libra: Divide and conquer to verify forwarding tables in huge networks","volume-title":"Proc. 11th USENIX Symp. Netw. Syst. Des. Implementation","author":"Zeng"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837657"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2013.6733614"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2716281.2836095"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"ref25","first-page":"735","article-title":"Delta-net: Real-time network verification using atoms","volume-title":"Proc. 14th USENIX Symp. Netw. Syst. Des. Implementation","author":"Horn"},{"key":"ref26","first-page":"241","article-title":"APKeep: Realtime verification for real networks","volume-title":"Proc. 17th USENIX Symp. Netw. Syst. Des. Implementation","author":"Zhang"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544246"},{"key":"ref28","first-page":"499","article-title":"Checking beliefs in dynamic networks","volume-title":"Proc. 12th USENIX Symp. Netw. Syst. Des. Implementation","author":"Lopes"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2017.2720172"},{"key":"ref30","first-page":"99","article-title":"Real time network policy checking using header space analysis","volume-title":"Proc. 10th USENIX Symp. Netw. Syst. Des. Implementation","author":"Kazemian"},{"key":"ref31","first-page":"601","article-title":"Differential network analysis","volume-title":"Proc. 19th USENIX Symp. Netw. Syst. Des. Implementation","author":"Zhang"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3610845"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_4"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2019.8888144"},{"key":"ref37","first-page":"617","article-title":"Katra: Realtime verification for multilayer networks","volume-title":"Proc. 19th USENIX Symp. Netw. Syst. Des. Implementation","author":"Beckett"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604843"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1734714.1734718"},{"article-title":"A BDD and Z-BDD library written in Java","year":"2020","author":"Vahidi","key":"ref40"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90034-2"},{"article-title":"Introducing data center fabric, the next-generation facebook data center network - Engineering at meta","year":"2014","author":"Andreyev","key":"ref42"},{"key":"ref43","first-page":"1","article-title":"Predicting the performance impact of different fat-tree configurations","volume-title":"Proc. Int. Conf. High Perform. Comput. Netw. Storage Anal.","author":"Jain"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM42981.2021.9488857"},{"article-title":"P4K: A formal semantics of P4 and applications","year":"2018","author":"Kheradmand","key":"ref45"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3434322"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/8858\/11077775\/10896588.pdf?arnumber=10896588","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T22:48:44Z","timestamp":1752274124000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10896588\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7]]},"references-count":45,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2025.3543437","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"type":"print","value":"1545-5971"},{"type":"electronic","value":"1941-0018"},{"type":"electronic","value":"2160-9209"}],"subject":[],"published":{"date-parts":[[2025,7]]}}}