{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T17:03:13Z","timestamp":1783098193960,"version":"3.54.6"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62102043"],"award-info":[{"award-number":["62102043"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Symbolic execution is a powerful technique for bug finding by generating test inputs to systematically explore all feasible paths within a given threshold. However, its practical usage is often limited by the\n            <jats:italic toggle=\"yes\">path explosion<\/jats:italic>\n            problem. In this paper, we propose compatible branch coverage driven symbolic execution for efficient bug finding. Our new technique owns a novel path-pruning strategy obtained from program dependency analysis to effectively avoid unnecessary explorations. Specifically, based on a\n            <jats:italic toggle=\"yes\">Compatible Branch Set<\/jats:italic>\n            , our technique directs symbolic execution to explore feasible branches while soundly pruning redundant paths that have no new contributions to branch coverage. We have implemented our approach atop KLEE and conducted experiments on a set of programs from Siemens Suite, GNU Coreutils, and other real-world programs. Experimental results show that, compared with the state-of-the-art symbolic execution techniques, our approach always uses significantly less time to reproduce bugs while achieving the same or better branch coverage. On average, our approach got over 45% path reduction and 3x speedup on the GNU Coreutils programs\n          <\/jats:p>","DOI":"10.1145\/3656443","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1633-1655","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-4680-4820","authenticated-orcid":false,"given":"Qiuping","family":"Yi","sequence":"first","affiliation":[{"name":"Beijing University of Posts and Telecommunications, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5894-5888","authenticated-orcid":false,"given":"Yifan","family":"Yu","sequence":"additional","affiliation":[{"name":"Beijing University of Posts and Telecommunications, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1404-4560","authenticated-orcid":false,"given":"Guowei","family":"Yang","sequence":"additional","affiliation":[{"name":"The University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Undefined Behavior Sanitizer. https:\/\/clang.llvm.org\/docs\/UndefinedBehaviorSanitizer.html#ubsan-checks"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_2"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534384"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393666"},{"key":"e_1_3_1_6_1","volume-title":"In USENIX Symposium on Operating Systems Design and Implementations. Berkeley, CA, USA, 209\u2013224","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 USENIX Symposium on Operating Systems Design and Implementations. Berkeley, CA, USA, 209\u2013224. https:\/\/doi.org\/10.5555\/1855741.1855756"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450087"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.simpa.2020.100038"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464815"},{"key":"e_1_3_1_10_1","unstructured":"Coreutils. August 2016. www.gnu.org\/software\/coreutils. (August 2016)"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-005-3861-2"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1450058.1450087"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428334"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484813"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416589"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-023-00310-8"},{"key":"e_1_3_1_19_1","volume-title":"Master\u2019s thesis. Computer Science Dept., University of Illinois at Urbana-Champaign, Urbana, IL","author":"Lattner Chris","year":"2002","unstructured":"Chris Lattner. 2002. LLVM: An Infrastructure for Multi-Stage Optimization. Master\u2019s thesis. Computer Science Dept., University of Illinois at Urbana-Champaign, Urbana, IL. http:\/\/llvm.cs.uiuc.edu"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC53868.2021.00051"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884845"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2522920.2522925"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_2"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.79"},{"key":"e_1_3_1_26_1","article-title":"Exploiting program dependencies for scalable multiple-path symbolic execution","author":"Santelices Raul","year":"2010","unstructured":"Raul Santelices and Mary Jean Harrold. 2010. Exploiting program dependencies for scalable multiple-path symbolic execution. In Proceedings of the 19th international symposium on Software testing and analysis. 195\u2013206. https:\/\/doi.org\/10.1145\/1831708.183173","journal-title":"In Proceedings of the 19th international symposium on Software testing and analysis. 195\u2013206"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_3"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384654"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001422"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180251"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3558919"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2584063"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER56733.2023.00023"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/bs.adcom.2018.10.002"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629536"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE55969.2022.00055"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2015.7102601"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2659751"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Qiuping Yi Yifan Yu and Guowe Yang. 2024. Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding. https:\/\/doi.org\/10.5281\/zenodo.1096092 10.5281\/zenodo.1096092","DOI":"10.5281\/zenodo.1096092"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656443","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656443","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:40:37Z","timestamp":1751661637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656443"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":39,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656443"],"URL":"https:\/\/doi.org\/10.1145\/3656443","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}