{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:15:00Z","timestamp":1766441700056,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":61,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3744826","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:32:38Z","timestamp":1763854358000},"page":"827-841","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Validating Interior Gateway Routing Protocols via Equivalent Topology Synthesis"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-8610-7946","authenticated-orcid":false,"given":"Bing","family":"Shui","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0610-8529","authenticated-orcid":false,"given":"Yufan","family":"Zhou","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3581-6832","authenticated-orcid":false,"given":"Jielun","family":"Wu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7743-1296","authenticated-orcid":false,"given":"Baowen","family":"Xu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8297-8998","authenticated-orcid":false,"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu, China"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"3255","volume-title":"Proceedings of the 31st USENIX Security Symposium (SEC '22)","author":"Ba Jinsheng","year":"2022","unstructured":"Jinsheng Ba, Marcel B\u00f6hme, Zahra Mirzamomen, and Abhik Roychoudhury. 2022. Stateful greybox fuzzing. In Proceedings of the 31st USENIX Security Symposium (SEC '22). USENIX Association, 3255-3272. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/ba"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2010.24"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1049\/cp:20080141"},{"key":"e_1_3_2_1_4_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08). USENIX Association, 209-224. https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"R. Callon. 1990. Use of OSI IS-IS for routing in TCP\/IP and dual environments. https:\/\/datatracker.ietf.org\/doc\/html\/rfc1195.","DOI":"10.17487\/rfc1195"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693074"},{"key":"e_1_3_2_1_7_1","unstructured":"Cisco. 2016. IP Routing: OSPF Configuration Guide. https:\/\/www.cisco.com\/c\/en\/us\/td\/docs\/ios-xml\/ios\/iproute_ospf\/configuration\/xe-16\/iro-xe-16-book\/iro-cfg.html."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ColComCon.2014.6860404"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"e_1_3_2_1_10_1","unstructured":"FRR Developers. 2024a. FRR RFC\/Compliance Test. https:\/\/github.com\/FRRouting\/frr\/wiki\/RFC_Compliance_Results\/OSPF_extended_results.pdf."},{"key":"e_1_3_2_1_11_1","unstructured":"FRR Developers. 2024b. FRR Topotests. https:\/\/github.com\/FRRouting\/frr\/tree\/master\/tests\/topotests."},{"key":"e_1_3_2_1_12_1","unstructured":"FRR Developers. 2024c. FRRouting Project. https:\/\/frrouting.org\/."},{"key":"e_1_3_2_1_13_1","unstructured":"Munet Developers. 2024d. Munet. https:\/\/github.com\/LabNConsulting\/munet."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Wesley Eddy. 2022. Transmission Control Protocol (TCP). https:\/\/datatracker.ietf.org\/doc\/html\/rfc9293.","DOI":"10.17487\/RFC9293"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472938"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_25"},{"key":"e_1_3_2_1_17_1","volume-title":"GDB: The GNU Project Debugger. https:\/\/www.sourceware.org\/gdb\/.","author":"GNU.","year":"2025","unstructured":"GNU. 2025. GDB: The GNU Project Debugger. https:\/\/www.sourceware.org\/gdb\/."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_3_2_1_19_1","unstructured":"Google. 2025. OSS-Fuzz. https:\/\/google.github.io\/oss-fuzz\/."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 22nd USENIX Conference on Security (SEC'13)","author":"Haller Istvan","year":"2013","unstructured":"Istvan Haller, Asia Slowinska, Matthias Neugschwandtner, and Herbert Bos. 2013. Dowsing for overflows: a guided fuzzer to find buffer boundary violations. In Proceedings of the 22nd USENIX Conference on Security (SEC'13). USENIX Association, 49\u201364. https:\/\/dl.acm.org\/doi\/10.5555\/2534766.2534772"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35533-7_16"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MASCOT.1998.693672"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35394-4_6"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00063"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/JCSSE.2017.8025919"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jnca.2017.09.006"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868447.1868466"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2022.3192991"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/PADS.2004.1301280"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1177\/0037549705055017"},{"key":"e_1_3_2_1_32_1","first-page":"4481","volume-title":"32nd USENIX Security Symposium (SEC '23)","author":"Luo Zhengxiong","year":"2023","unstructured":"Zhengxiong Luo, Junze Yu, Feilong Zuo, Jianzhong Liu, Yu Jiang, Ting Chen, Abhik Roychoudhury, and Jiaguang Sun. 2023. Bleem: packet sequence oriented fuzzing for protocol implementations. In 32nd USENIX Security Symposium (SEC '23). USENIX Association, 4481-4498. https:\/\/dl.acm.org\/doi\/10.5555\/3620237.3620488"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2007.10.031"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1163653.1163663"},{"key":"e_1_3_2_1_35_1","unstructured":"Saif Ur Rehman Malik. 2014. Using formal methods to validate the usage protocols and feasibility in large scale computing systems. Ph.D. Dissertation. North Dakota State University. https:\/\/core.ac.uk\/download\/pdf\/211302484.pdf#page=123"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7777970"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2024.24556"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"John Moy. 1998. OSPF Version 2. https:\/\/datatracker.ietf.org\/doc\/html\/rfc2328.","DOI":"10.17487\/rfc2328"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 1st Conference on Symposium on Networked Systems Design and Implementation -","volume":"1","author":"Musuvathi Madanlal","unstructured":"Madanlal Musuvathi and Dawson R. Engler. 2004. Model checking large network protocol implementations. In Proceedings of the 1st Conference on Symposium on Networked Systems Design and Implementation - Volume 1 (NSDI'04). USENIX Association, 12. https:\/\/dl.acm.org\/doi\/10.5555\/1251175.1251187"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/844128.844136"},{"key":"e_1_3_2_1_41_1","unstructured":"Ameet Naik. 2018. Anatomy of a BGP Hijack on Amazon's Route 53 DNS Service. https:\/\/www.thousandeyes.com\/blog\/amazon-route-53-dns-and-bgp-hijack."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-022-10233-3"},{"key":"e_1_3_2_1_43_1","volume-title":"EIGRP network design solutions","author":"Pepelnjak Ivan","year":"1947","unstructured":"Ivan Pepelnjak. 1999. EIGRP network design solutions. Cisco Press. https:\/\/dl.acm.org\/doi\/10.5555\/519477"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST46399.2020.00062"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580598"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/98.760423"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616614"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192418"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/3620237.3620630"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/AST.2007.1"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643762"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3565800"},{"key":"e_1_3_2_1_53_1","first-page":"131545","volume-title":"LLMDFA: Analyzing Dataflow in Code with Large Language Models. In Advances in Neural Information Processing Systems (NEURIPS '24)","author":"Wang Chengpeng","year":"2024","unstructured":"Chengpeng Wang, Wuqi Zhang, Zian Su, Xiangzhe Xu, Xiaoheng Xie, and Xiangyu Zhang. 2024. LLMDFA: Analyzing Dataflow in Code with Large Language Models. In Advances in Neural Information Processing Systems (NEURIPS '24). Curran Associates, Inc., 131545-131574."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_3_2_1_55_1","unstructured":"Oskar Wibling. 2005. Ad hoc routing protocol validation. Ph.D. Dissertation. Uppsala University. https:\/\/uu.diva-portal.org\/smash\/get\/diva2:117170\/FULLTEXT01.pdf"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/1764575.1764582"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3485363"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/0-306-47003-9_7"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICON.2001.962339"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649854"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3744826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:11:15Z","timestamp":1766441475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3744826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":61,"alternative-id":["10.1145\/3719027.3744826","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3744826","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}