{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T23:28:44Z","timestamp":1784590124574,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,7]],"date-time":"2022-11-07T00:00:00Z","timestamp":1667779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"the National Research Foundation (NRF) Singapore and National Satellite of Excellence in Trustworthy Software Systems (NSoE-TSS)","award":["NSOE-TSS2019-04"],"award-info":[{"award-number":["NSOE-TSS2019-04"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,11,7]]},"DOI":"10.1145\/3540250.3558919","type":"proceedings-article","created":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T20:46:22Z","timestamp":1668026782000},"page":"1741-1745","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["FastKLEE: faster symbolic execution via reducing redundant bound checking of type-safe pointers"],"prefix":"10.1145","author":[{"given":"Haoxin","family":"Tu","sequence":"first","affiliation":[{"name":"Singapore Management University, Singapore \/ Dalian University of Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lingxiao","family":"Jiang","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuhua","family":"Ding","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"He","family":"Jiang","sequence":"additional","affiliation":[{"name":"Dalian University of Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,11,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560217.2560219"},{"key":"e_1_3_2_1_2_1","volume-title":"Camil Demetrescu, and Irene Finocchi.","author":"Baldoni Roberto","year":"2018","unstructured":"Roberto Baldoni , Emilio Coppa , Daniele Cono D\u2019elia , Camil Demetrescu, and Irene Finocchi. 2018 . A Survey of Symbolic Execution Techniques. ACM Comput. Surv., 51, 3 (2018), Article 50, 39 pages. issn:0360-0300 Roberto Baldoni, Emilio Coppa, Daniele Cono D\u2019elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Comput. Surv., 51, 3 (2018), Article 50, 39 pages. issn:0360-0300"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397360"},{"key":"e_1_3_2_1_4_1","volume-title":"Type Inference on Executables. ACM Comput. Surv., 48, 4","author":"Caballero Juan","year":"2016","unstructured":"Juan Caballero and Zhiqiang Lin . 2016. Type Inference on Executables. ACM Comput. Surv., 48, 4 ( 2016 ), Article 65, 35 pages. issn:0360-0300 Juan Caballero and Zhiqiang Lin. 2016. Type Inference on Executables. ACM Comput. Surv., 48, 4 (2016), Article 65, 35 pages. issn:0360-0300"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 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 Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209\u2013224 . 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. 209\u2013224."},{"key":"e_1_3_2_1_6_1","volume-title":"Unleashing Mayhem on Binary Code. In 2012 IEEE Symposium on Security and Privacy. 380\u2013394","author":"Cha Sang Kil","year":"2012","unstructured":"Sang Kil Cha , Thanassis Avgerinos , Alexandre Rebert , and David Brumley . 2012 . Unleashing Mayhem on Binary Code. In 2012 IEEE Symposium on Security and Privacy. 380\u2013394 . Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. 2012. Unleashing Mayhem on Binary Code. In 2012 IEEE Symposium on Security and Privacy. 380\u2013394."},{"key":"e_1_3_2_1_7_1","unstructured":"Junjie Chen Wenxiang Hu Lingming Zhang Dan Hao Sarfraz Khurshid and Lu Zhang. 2018. Learning to Accelerate Symbolic Execution via Code Transformation. In ECOOP. \t\t\t\t  Junjie Chen Wenxiang Hu Lingming Zhang Dan Hao Sarfraz Khurshid and Lu Zhang. 2018. Learning to Accelerate Symbolic Execution via Code Transformation. In ECOOP."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950396"},{"key":"e_1_3_2_1_9_1","unstructured":"KLEE Official Document. 2022. Instruction for building GNU Coreutils. http:\/\/klee.github.io\/tutorials\/testing-coreutils\/ \t\t\t\t  KLEE Official Document. 2022. Instruction for building GNU Coreutils. http:\/\/klee.github.io\/tutorials\/testing-coreutils\/"},{"key":"e_1_3_2_1_10_1","unstructured":"KLEE Official Document. 2022. Instruction for selecting running options. http:\/\/klee.github.io\/docs\/coreutils-experiments\/ \t\t\t\t  KLEE Official Document. 2022. Instruction for selecting running options. http:\/\/klee.github.io\/docs\/coreutils-experiments\/"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2015.7381814"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484813"},{"key":"e_1_3_2_1_13_1","unstructured":"Kaiming Huang Yongzhe Huang Mathias Payer Zhiyun Qian Jack Sampson Gang Tan and Trent Jaeger. 2022. DataGuard Repo. \t\t\t\t  Kaiming Huang Yongzhe Huang Mathias Payer Zhiyun Qian Jack Sampson Gang Tan and Trent Jaeger. 2022. DataGuard Repo."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2022.23060"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314610"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Volodymyr Kuznetsov Johannes Kinder Stefan Bucur and George Candea. 2012. Efficient State Merging in Symbolic Execution. 193\u2013204. isbn:9781450312059 \t\t\t\t  Volodymyr Kuznetsov Johannes Kinder Stefan Bucur and George Candea. 2012. Efficient State Merging in Symbolic Execution. 193\u2013204. isbn:9781450312059","DOI":"10.1145\/2345156.2254088"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509553"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3052973.3053014"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_3_2_1_21_1","unstructured":"David M. Perry Andrea Mattavelli Xiangyu Zhang and Cristian Cadar. 2017. Accelerating Array Constraints in Symbolic Execution. 68\u201378. isbn:9781450350761 \t\t\t\t  David M. Perry Andrea Mattavelli Xiangyu Zhang and Cristian Cadar. 2017. Accelerating Array Constraints in Symbolic Execution. 68\u201378. isbn:9781450350761"},{"key":"e_1_3_2_1_22_1","first-page":"17","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon . 2020 . Symbolic execution with SymCC: Don\u2019 t interpret, compile! . In 29th USENIX Security Symposium (USENIX Security 20) . 181\u2013198. isbn:978-1-939133- 17 - 15 Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: Don\u2019 t interpret, compile!. In 29th USENIX Security Symposium (USENIX Security 20). 181\u2013198. isbn:978-1-939133-17-5"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2021. SymQEMU: Compilation-based symbolic execution for binaries. In NDSS. \t\t\t\t  Sebastian Poeplau and Aur\u00e9lien Francillon. 2021. SymQEMU: Compilation-based symbolic execution for binaries. In NDSS.","DOI":"10.14722\/ndss.2021.24118"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_2_1_25_1","unstructured":"STP. 2022. Simple Theorem Prover an efficient SMT solver for bitvectors. https:\/\/github.com\/stp\/stp \t\t\t\t  STP. 2022. Simple Theorem Prover an efficient SMT solver for bitvectors. https:\/\/github.com\/stp\/stp"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468596"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180251"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397363"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913)","author":"Wagner Jonas","year":"2013","unstructured":"Jonas Wagner , Volodymyr Kuznetsov , and George Candea . 2013 . Overify: Optimizing Programs for Fast Verification . In Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913) . 1\u201318. Jonas Wagner, Volodymyr Kuznetsov, and George Candea. 2013. Overify: Optimizing Programs for Fast Verification. In Proceedings of the 14th USENIX Conference on Hot Topics in Operating Systems (HotOS\u201913). 1\u201318."},{"key":"e_1_3_2_1_30_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Yun Insu","year":"2018","unstructured":"Insu Yun , Sangho Lee , Meng Xu , Yeongjin Jang , and Taesoo Kim . 2018 . QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing . In 27th USENIX Security Symposium (USENIX Security 18) . Baltimore, MD. 745\u2013761. isbn:978-1-939133-04-5 Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2018. QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing. In 27th USENIX Security Symposium (USENIX Security 18). Baltimore, MD. 745\u2013761. isbn:978-1-939133-04-5"},{"key":"e_1_3_2_1_31_1","unstructured":"Z3. 2022. A theorem prover from Microsoft Research. https:\/\/github.com\/z3prover\/z3 \t\t\t\t  Z3. 2022. A theorem prover from Microsoft Research. https:\/\/github.com\/z3prover\/z3"}],"event":{"name":"ESEC\/FSE '22: 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Singapore Singapore","acronym":"ESEC\/FSE '22","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","NUS NUS"]},"container-title":["Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3540250.3558919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3540250.3558919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:03Z","timestamp":1750182543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3540250.3558919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,7]]},"references-count":31,"alternative-id":["10.1145\/3540250.3558919","10.1145\/3540250"],"URL":"https:\/\/doi.org\/10.1145\/3540250.3558919","relation":{},"subject":[],"published":{"date-parts":[[2022,11,7]]},"assertion":[{"value":"2022-11-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}