{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T00:48:34Z","timestamp":1740185314104,"version":"3.37.3"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","funder":[{"name":"National Natural Science Foundation of China","award":["62172429, 62032024, 62372162"]},{"name":"National Key Research and Development Program of China","award":["2022YFB4501903"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2024,7,12]]},"abstract":"Constraint solving is one of the main challenges for symbolic execution. Caching is an effective mechanism to reduce the number of the solver invocations in symbolic execution and is adopted by many mainstream symbolic execution engines. However, caching can not perform well on all programs. How to improve caching\u2019s effectiveness is challenging in general. In this work, we propose a partial solution-based caching method for improving caching\u2019s effectiveness. Our key idea is to utilize the partial solutions inside the constraint solving to generate more cache entries. A partial solution may satisfy other constraints of symbolic execution. Hence, our partial solution-based caching method naturally improves the rate of cache hits. We have implemented our method on two mainstream symbolic executors (KLEE and Symbolic PathFinder) and two SMT solvers (STP and Z3). The results of extensive experiments on real-world benchmarks demonstrate that our method effectively increases the number of the explored paths in symbolic execution. Our caching method achieves 1.07x to 2.3x speedups for exploring the same amount of paths on different benchmarks.<\/jats:p>","DOI":"10.1145\/3660817","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T14:22:09Z","timestamp":1720794129000},"page":"2493-2514","source":"Crossref","is-referenced-by-count":0,"title":["Partial Solution Based Constraint Solving Cache in Symbolic Execution"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0575-5074","authenticated-orcid":false,"given":"Ziqi","family":"Shuai","sequence":"first","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4066-7892","authenticated-orcid":false,"given":"Zhenbang","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1874-4820","authenticated-orcid":false,"given":"Kelin","family":"Ma","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4384-430X","authenticated-orcid":false,"given":"Kunlin","family":"Liu","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6082-4501","authenticated-orcid":false,"given":"Yufeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Hunan University, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2024,7,12]]},"reference":[{"volume-title":"https:\/\/en.wikipedia.org\/wiki\/Equisatisfiability. Accessed","year":"2023","key":"e_1_2_1_1_1","unstructured":"2023. Equisatisfiability. https:\/\/en.wikipedia.org\/wiki\/Equisatisfiability. Accessed September 25, 2023"},{"volume-title":"Accessed","year":"2023","key":"e_1_2_1_2_1","unstructured":"2023. GNU Scientific Library. https:\/\/www.gnu.org\/software\/gsl\/. Accessed September 25, 2023"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771802"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.46"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106303"},{"key":"e_1_2_1_7_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. 209\u2013224."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464815"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. 15\u201344. https:\/\/doi.org\/10.1007\/978-3-642-36675-8_2 10.1007\/978-3-642-36675-8_2","DOI":"10.1007\/978-3-642-36675-8_2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.26"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-64410-3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_2_1_18_1","volume-title":"Patterson","author":"Hennessy John L.","year":"2012","unstructured":"John L. Hennessy and David A. Patterson. 2012. Computer Architecture - A Quantitative Approach, 5th Edition. Morgan Kaufmann. isbn:978-0-12-383872-8","edition":"5"},{"key":"e_1_2_1_19_1","first-page":"467","volume-title":"Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99","author":"Hoffmann J\u00f6rg","year":"1999","unstructured":"J\u00f6rg Hoffmann and Jana Koehler. 1999. A New Method to Index and Query Sets. In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, 1450 pages, Thomas Dean (Ed.). Morgan Kaufmann, 462\u2013467. http:\/\/ijcai.org\/Proceedings\/99-1\/Papers\/067.pdf"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115670"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_21"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092728"},{"key":"e_1_2_1_28_1","volume-title":"29th USENIX Security Symposium, USENIX Security 2020","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: Don\u2019t interpret, compile!. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020. 181\u2013198."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464826"},{"key":"e_1_2_1_30_1","unstructured":"Jan Taljaard. 2019. Optimised constraint solving for real-world problems."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_15"},{"key":"e_1_2_1_32_1","volume-title":"TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings, Bernhard Beckert and Reiner H\u00e4hnle (Eds.) (Lecture Notes in Computer Science","volume":"153","author":"Tillmann Nikolai","year":"2008","unstructured":"Nikolai Tillmann and Jonathan de Halleux. 2008. Pex-White Box Test Generation for .NET. In Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings, Bernhard Beckert and Reiner H\u00e4hnle (Eds.) (Lecture Notes in Computer Science, Vol. 4966). Springer, 134\u2013153."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST49551.2021.00023"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_1_35_1","volume-title":"27th USENIX Security Symposium, USENIX Security 2018","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 2018, Baltimore, MD, USA, August 15-17, 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 745\u2013761."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416645"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2012.8"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3660817","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,19]],"date-time":"2024-08-19T18:28:40Z","timestamp":1724092120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660817"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,12]]},"references-count":37,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2024,7,12]]}},"alternative-id":["10.1145\/3660817"],"URL":"https:\/\/doi.org\/10.1145\/3660817","relation":{},"ISSN":["2994-970X"],"issn-type":[{"type":"electronic","value":"2994-970X"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}