{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T04:32:57Z","timestamp":1727065977589},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"Countless devices all over the world are connected by networks and communicated via network protocols. Just like common software, protocol implementations suffer from bugs, many of which only cause silent data corruption instead of crashes. Hence, existing automated bug-finding techniques focused on memory safety, such as fuzzing, can hardly detect them. In this work, we propose a static differential analysis called ParDiff to find protocol implementation bugs, especially silent ones hidden in message parsers. Our key observation is that a network protocol often has multiple implementations and any semantic discrepancy between them may indicate bugs. However, different implementations are often written in disparate styles, e.g., using different data structures or written with different control structures, making it challenging to directly compare two implementations of even the same protocol. To exploit this observation and effectively compare multiple protocol implementations, ParDiff (1) automatically extracts finite state machines from programs to represent protocol format specifications, and (2) then leverages bisimulation and SMT solvers to find fine-grained and \nsemantic inconsistencies between them. We have extensively evaluated ParDiff using 14 network protocols. The results show that ParDiff outperforms both differential symbolic execution and differential fuzzing tools. To date, we have detected 41 bugs with 25 confirmed by developers.<\/jats:p>","DOI":"10.1145\/3649854","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1208-1234","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["ParDiff: Practical Static Differential Analysis of Network Protocol Parsers"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"http:\/\/orcid.org\/0009-0003-6032-6045","authenticated-orcid":false,"given":"Mingwei","family":"Zheng","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-8297-8998","authenticated-orcid":false,"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0000-5319-1160","authenticated-orcid":false,"given":"Xuwei","family":"Liu","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-6619-781X","authenticated-orcid":false,"given":"Xiangzhe","family":"Xu","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0008-7613-946X","authenticated-orcid":false,"given":"Le","family":"Yu","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-5774-0809","authenticated-orcid":false,"given":"Congyu","family":"Liu","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-3150-2033","authenticated-orcid":false,"given":"Guannan","family":"Wei","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-9544-2500","authenticated-orcid":false,"given":"Xiangyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Fernando Arnaboldi. 2023. XDiFF. https:\/\/github.com\/IOActive\/XDiFF"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 30th International Conference on Software Engineering (ICSE \u201908)","author":"Babic Domagoj","unstructured":"Domagoj Babic and Alan J. Hu. 2008. Calysto: scalable and precise extended static checking. In Proceedings of the 30th International Conference on Software Engineering (ICSE \u201908). ACM, 211\u2013220. https:\/\/doi.org\/10.1145\/1368088.1368118 10.1145\/1368088.1368118"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920)","author":"Badihi Sahar","year":"2020","unstructured":"Sahar Badihi, Faridah Akinotcho, Yi Li, and Julia Rubin. 2020. ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920). ACM, 13\u201324. https:\/\/doi.org\/10.1145\/3368089.3409757 10.1145\/3368089.3409757"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916)","author":"Bao Wenlei","year":"2016","unstructured":"Wenlei Bao, Sriram Krishnamoorthy, Louis-No\u00ebl Pouchet, Fabrice Rastello, and P Sadayappan. 2016. PolyCheck: dynamic verification of iteration space transformations on affine programs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201916). ACM, 539\u2013554. https:\/\/doi.org\/10.1145\/2837614.2837656 10.1145\/2837614.2837656"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201917)","author":"Bastani Osbert","year":"2017","unstructured":"Osbert Bastani, Rahul Sharma, Alex Aiken, and Percy Liang. 2017. Synthesizing Program Input Grammars. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201917). ACM, 95\u2013110. https:\/\/doi.org\/10.1145\/3062341.3062349 10.1145\/3062341.3062349"},{"key":"e_1_2_1_7_1","volume-title":"Replication Study. In Proceedings of the th International Conference on Software Engineering (PLDI \u201922)","author":"Bendrissou Bachir","year":"2022","unstructured":"Bachir Bendrissou, Rahul Gopinath, and Andreas Zeller. 2022. \u201cSynthesizing Input Grammars\u201d: A Replication Study. In Proceedings of the th International Conference on Software Engineering (PLDI \u201922). ACM, 260\u2013268. https:\/\/doi.org\/10.1145\/3519939.3523716 10.1145\/3519939.3523716"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-457"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 16th ACM conference on Computer and communications security (CCS \u201909)","author":"Caballero Juan","year":"2009","unstructured":"Juan Caballero, Pongsin Poosankam, Christian Kreibich, and Dawn Song. 2009. Dispatcher: Enabling active botnet infiltration using automatic protocol reverse-engineering. In Proceedings of the 16th ACM conference on Computer and communications security (CCS \u201909). ACM, 621\u2013634. https:\/\/doi.org\/10.1145\/1653662.1653737 10.1145\/1653662.1653737"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201908)","author":"Cadar Cristian","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201908). USENIX, 209\u2013224. https:\/\/www.usenix.org\/conference\/osdi-08\/klee-unassisted-and-automatic-generation-high-coverage-tests-complex-systems"},{"key":"e_1_2_1_11_1","volume-title":"Companion Proceedings of the 36th International Conference on Software Engineering (ICSE Companion \u201914)","author":"Cadar Cristian","year":"2014","unstructured":"Cristian Cadar and Hristina Palikareva. 2014. Shadow symbolic execution for better testing of evolving software. In Companion Proceedings of the 36th International Conference on Software Engineering (ICSE Companion \u201914). ACM, 432\u2013435. https:\/\/doi.org\/10.1145\/2591062.2591104 10.1145\/2591062.2591104"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201913)","author":"Cho Chia Yuan","year":"2013","unstructured":"Chia Yuan Cho, Vijay D\u2019Silva, and Dawn Song. 2013. BLITZ: Compositional bounded model checking for real-world programs. In Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201913). IEEE, 136\u2013146. https:\/\/doi.org\/10.1109\/ASE.2013.6693074 10.1109\/ASE.2013.6693074"},{"key":"e_1_2_1_13_1","unstructured":"Juliusz Chroboczek. 2023. parse_update_subtlv in Jech. https:\/\/github.com\/jech\/babeld\/blob\/babeld-1.12-branch\/message.c"},{"key":"e_1_2_1_14_1","unstructured":"Juliusz Chroboczek and David Schinazi. 2023. RFC 8966: The Babel Routing Protocol. https:\/\/www.rfc-editor.org\/rfc\/rfc8966.html"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201919)","author":"Churchill Berkeley","year":"2019","unstructured":"Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. 2019. Semantic program alignment for equivalence checking. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201919). ACM, 1027\u20131040. https:\/\/doi.org\/10.1145\/3314221.3314596 10.1145\/3314221.3314596"},{"key":"e_1_2_1_16_1","unstructured":"FRR community. 2023. The FRRouting protocol suite. https:\/\/github.com\/FRRouting\/frr"},{"key":"e_1_2_1_17_1","unstructured":"Wikipedia contributors. 2022. List of open-source routing platforms. https:\/\/wikipedia.org\/wiki\/List_of_open-source_routing_platforms"},{"key":"e_1_2_1_18_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908","volume":"340","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201908, Vol. 4963). Springer, 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_19_1","unstructured":"FRR Developers. 2023. FRRouting. https:\/\/github.com\/FRRouting\/frr\/blob\/ab68283ceedc05ea1a7f9c54f03a87f5dc199a01\/babeld\/message.c"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 2021 ACM SIGCOMM 2021 Conference (SIGCOMM \u201921)","author":"Ferreira Tiago","year":"2021","unstructured":"Tiago Ferreira, Harrison Brewton, Loris D\u2019Antoni, and Alexandra Silva. 2021. Prognosis: closed-box analysis of network protocol implementations. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference (SIGCOMM \u201921). ACM, 762\u2013774. https:\/\/doi.org\/10.1145\/3452296.3472938 10.1145\/3452296.3472938"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_25"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027328830731"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920)","author":"Gopinath Rahul","year":"2020","unstructured":"Rahul Gopinath, Bj\u00f6rn Mathis, and Andreas Zeller. 2020. Mining Input Grammars from Dynamic Control Flow. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201920). ACM, 172\u2013183. https:\/\/doi.org\/10.1145\/3368089.3409679 10.1145\/3368089.3409679"},{"key":"e_1_2_1_25_1","volume-title":"22nd USENIX Security Symposium (USENIX Security \u201913)","author":"Haller Istvan","year":"2013","unstructured":"Istvan Haller, Asia Slowinska, Matthias Neugschwandtner, and Herbert Bos. 2013. Dowser: a guided fuzzer to find buffer overflow vulnerabilities. In 22nd USENIX Security Symposium (USENIX Security \u201913). USENIX, 49\u201364. https:\/\/www.usenix.org\/conference\/usenixsecurity13\/technical-sessions\/papers\/haller"},{"key":"e_1_2_1_26_1","unstructured":"Heartbleed. 2020. The Heartbleed Bug. https:\/\/heartbleed.com"},{"key":"e_1_2_1_27_1","volume-title":"2020 IEEE Symposium on Security and Privacy (S&P \u201920)","author":"Huang Heqing","year":"2020","unstructured":"Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang. 2020. Pangolin: Incremental hybrid fuzzing with polyhedral path abstraction. In 2020 IEEE Symposium on Security and Privacy (S&P \u201920). IEEE, 1613\u20131627. https:\/\/doi.org\/10.1109\/SP40000.2020.00063 10.1109\/SP40000.2020.00063"},{"key":"e_1_2_1_28_1","volume-title":"Differential Slicing: Identifying Causal Execution Differences for Security Applications. In 2011 IEEE Symposium on Security and Privacy (S&P \u201911)","author":"Johnson Noah M.","year":"2011","unstructured":"Noah M. Johnson, Juan Caballero, Kevin Zhijie Chen, Stephen McCamant, Pongsin Poosankam, Daniel Reynaud, and Dawn Song. 2011. Differential Slicing: Identifying Causal Execution Differences for Security Applications. In 2011 IEEE Symposium on Security and Privacy (S&P \u201911). IEEE, 347\u2013362. https:\/\/doi.org\/10.1109\/SP.2011.41 10.1109\/SP.2011.41"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0171-7"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE \u201913)","author":"Lahiri Shuvendu K.","year":"2013","unstructured":"Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel. 2013. Differential Assertion Checking. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (ESEC\/FSE \u201913). ACM, 345\u2013355. https:\/\/doi.org\/10.1145\/2491411.2491452 10.1145\/2491411.2491452"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Symposium on Code Generation and Optimization (CGO \u201904)","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization (CGO \u201904). IEEE, 75. https:\/\/doi.org\/10.1109\/CGO.2004.1281665 10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453114"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2644805"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201918)","author":"Ma Shiqing","year":"2018","unstructured":"Shiqing Ma, Yingqi Liu, Wen-Chuan Lee, Xiangyu Zhang, and Ananth Grama. 2018. MODE: automated neural network model debugging via state differential analysis and input selection. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201918). ACM, 175\u2013186. https:\/\/doi.org\/10.1145\/3236024.3236082 10.1145\/3236024.3236082"},{"key":"e_1_2_1_36_1","volume-title":"2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST \u201921)","author":"Mal\u00edk Viktor","year":"2021","unstructured":"Viktor Mal\u00edk and Tom\u00e1\u0161 Vojnar. 2021. Automatically checking semantic equivalence between versions of large-scale C projects. In 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST \u201921). IEEE, 329\u2013339. https:\/\/doi.org\/10.1109\/ICST49551.2021.00045 10.1109\/ICST49551.2021.00045"},{"key":"e_1_2_1_37_1","unstructured":"Mares Martin Machek Pavel Filip Ondrej and CZ.NIC.. 2023. BIRD internet routing daemon. https:\/\/gitlab.nic.cz\/labs\/bird"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201918)","author":"Mora Federico","year":"2018","unstructured":"Federico Mora, Yi Li, Julia Rubin, and Marsha Chechik. 2018. Client-specific equivalence checking. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering (ASE \u201918). ACM, 441\u2013451. https:\/\/doi.org\/10.1145\/3238147.3238178 10.1145\/3238147.3238178"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 1st USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201904)","author":"Musuvathi Madanlal","unstructured":"Madanlal Musuvathi and Dawson R. Engler. 2004. Model Checking Large Network Protocol Implementations. In Proceedings of the 1st USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201904). USENIX, 12. https:\/\/doi.org\/10.1145\/3092282.3092289 10.1145\/3092282.3092289"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 42nd International Conference on Software Engineering (ICSE \u201920)","author":"Noller Yannic","year":"2020","unstructured":"Yannic Noller, Corina S P\u0103s\u0103reanu, Marcel B\u00f6hme, Youcheng Sun, Hoang Lam Nguyen, and Lars Grunske. 2020. HyDiff: Hybrid differential software analysis. In Proceedings of the 42nd International Conference on Software Engineering (ICSE \u201920). ACM, 1273\u20131285. https:\/\/doi.org\/10.1145\/3377811.3380363 10.1145\/3377811.3380363"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 38th International Conference on Software Engineering (ICSE \u201916)","author":"Palikareva Hristina","year":"2016","unstructured":"Hristina Palikareva, Tomasz Kuchta, and Cristian Cadar. 2016. Shadow of a doubt: testing for divergences between software versions. In Proceedings of the 38th International Conference on Software Engineering (ICSE \u201916). ACM, 1181\u20131192. https:\/\/doi.org\/10.1145\/2884781.2884845 10.1145\/2884781.2884845"},{"key":"e_1_2_1_42_1","unstructured":"Joshua Pereyda. 2023. BooFuzz. https:\/\/github.com\/jtpereyda\/boofuzz"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT \u201908\/FSE \u201916)","author":"Person Suzette","unstructured":"Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. Pundefinedsundefinedreanu. 2008. Differential Symbolic Execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT \u201908\/FSE \u201916). ACM, 226\u2013237. https:\/\/doi.org\/10.1145\/1453101.1453131 10.1145\/1453101.1453131"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201911)","author":"Person Suzette","year":"2011","unstructured":"Suzette Person, Guowei Yang, Neha Rungta, and Sarfraz Khurshid. 2011. Directed Incremental Symbolic Execution. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201911). ACM, 504\u2013515. https:\/\/doi.org\/10.1145\/1993498.1993558 10.1145\/1993498.1993558"},{"key":"e_1_2_1_45_1","volume-title":"2017 IEEE Symposium on security and privacy (S&P \u201917)","author":"Petsios Theofilos","year":"2017","unstructured":"Theofilos Petsios, Adrian Tang, Salvatore Stolfo, Angelos D Keromytis, and Suman Jana. 2017. Nezha: Efficient domain-independent differential testing. In 2017 IEEE Symposium on security and privacy (S&P \u201917). IEEE, 615\u2013632. https:\/\/doi.org\/10.1109\/SP.2017.27 10.1109\/SP.2017.27"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_55"},{"key":"e_1_2_1_47_1","volume-title":"Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In 24th USENIX Security Symposium (USENIX Security \u201915)","author":"David","unstructured":"David A. Ramos and Dawson R. Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In 24th USENIX Security Symposium (USENIX Security \u201915). USENIX, 49\u201364. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/ramos"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 36th Annual Computer Security Applications Conference (ACSAC \u201920)","author":"Reen Gaganjeet Singh","year":"2020","unstructured":"Gaganjeet Singh Reen and Christian Rossow. 2020. DPIFuzz: a differential fuzzing framework to detect DPI elusion strategies for QUIC. In Proceedings of the 36th Annual Computer Security Applications Conference (ACSAC \u201920). ACM, 332\u2013344. https:\/\/doi.org\/10.1145\/3427228.3427662 10.1145\/3427228.3427662"},{"key":"e_1_2_1_49_1","volume-title":"Automating Differential Testing with Overapproximate Symbolic Execution. In 2022 15th IEEE Conference on Software Testing, Verification and Validation (ICST \u201922)","author":"Rutledge Richard","year":"2022","unstructured":"Richard Rutledge and Alessandro Orso. 2022. Automating Differential Testing with Overapproximate Symbolic Execution. In 2022 15th IEEE Conference on Software Testing, Verification and Validation (ICST \u201922). IEEE, 256\u2013266. https:\/\/doi.org\/10.1109\/ICST53961.2022.00035 10.1109\/ICST53961.2022.00035"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1017\/S0960129598002527","article-title":"On the bisimulation proof method","volume":"8","author":"Sangiorgi Davide","year":"1998","unstructured":"Davide Sangiorgi. 1998. On the bisimulation proof method. Mathematical Structures in Computer Science, 8 (1998), 447 \u2013 479. https:\/\/api.semanticscholar.org\/CorpusID:14986397","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS \u201923)","author":"Shi Qingkai","year":"2023","unstructured":"Qingkai Shi, Junyang Shao, Yapeng Ye, Mingwei Zheng, and Xiangyu Zhang. 2023. Lifting Network Protocol Implementation to Precise Format Specification with Security Applications. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS \u201923). ACM, 1287\u20131301. https:\/\/doi.org\/10.1145\/3576915.3616614 10.1145\/3576915.3616614"},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201918)","author":"Shi Qingkai","year":"2018","unstructured":"Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. 2018. Pinpoint: Fast and precise sparse value flow analysis for million lines of code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201918). ACM, 693\u2013706. https:\/\/doi.org\/10.1145\/3192366.3192418 10.1145\/3192366.3192418"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS \u201911)","author":"Sui Yulei","year":"2011","unstructured":"Yulei Sui, Sen Ye, Jingling Xue, and Pen-Chung Yew. 2011. SPAS: Scalable path-sensitive pointer analysis on full-sparse SSA. In Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS \u201911). Springer, 155\u2013171. https:\/\/doi.org\/10.1007\/978-3-642-25318-8_14 10.1007\/978-3-642-25318-8_14"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362390"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the 38th International Conference on Software Engineering (ICSE \u201923)","author":"Wei Guannan","year":"2023","unstructured":"Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bracevac, and Tiark Rompf. 2023. Compiling Parallel Symbolic Execution with Continuations. In Proceedings of the 38th International Conference on Software Engineering (ICSE \u201923). IEEE, 1316\u20131328. https:\/\/doi.org\/10.1109\/ICSE48619.2023.00116 10.1109\/ICSE48619.2023.00116"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201905)","author":"Xie Yichen","year":"2005","unstructured":"Yichen Xie and Alex Aiken. 2005. Scalable error detection using Boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201905). ACM, 351\u2013363. https:\/\/doi.org\/10.1145\/1047659.1040334 10.1145\/1047659.1040334"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201921)","author":"Yang Youngseok","year":"2021","unstructured":"Youngseok Yang, Taesoo Kim, and Byung-Gon Chun. 2021. Finding consensus bugs in ethereum via multi-transaction differential fuzzing. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201921). USENIX, 349\u2013365. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yang"},{"key":"e_1_2_1_58_1","volume-title":"TCP-Fuzz: Detecting Memory and Semantic Bugs in TCP Stacks with Fuzzing. In USENIX Annual Technical Conference (ATC \u201921)","author":"Zou Yong-Hao","year":"2021","unstructured":"Yong-Hao Zou, Jia-Ju Bai, Jielong Zhou, Jianfeng Tan, Chenggang Qin, and Shi-Min Hu. 2021. TCP-Fuzz: Detecting Memory and Semantic Bugs in TCP Stacks with Fuzzing. In USENIX Annual Technical Conference (ATC \u201921). USENIX, 489\u2013502. https:\/\/www.usenix.org\/conference\/atc21\/presentation\/zou"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T18:05:11Z","timestamp":1714413911000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":58,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649854"],"URL":"https:\/\/doi.org\/10.1145\/3649854","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}