{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T15:22:08Z","timestamp":1770996128402,"version":"3.50.1"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"DOI":"10.13039\/501100001809","name":"National Science Foundation of China","doi-asserted-by":"crossref","award":["62293511"],"award-info":[{"award-number":["62293511"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Key R&D Program of Zhejiang","award":["2025C01083"],"award-info":[{"award-number":["2025C01083"]}]},{"name":"Ministry of Education, Singapore, under its Academic Research Fund Tier 2","award":["T2EP20222-0037"],"award-info":[{"award-number":["T2EP20222-0037"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    Symbolic execution is a powerful technique that can accurately synthesize program inputs for program testing through constraint solving. Applying symbolic execution effectively means that we must solve two searching problems efficiently. One is to search through the many program paths and the other is, given a particular path condition, to search through the numerous variable assignments to identify one satisfying solution. With few exceptions, existing symbolic execution engines treat constraint solvers as black boxes. As a result, the two searches are completely separated, which results in much redundancy (i.e., the same variable assignments may be tried for solving many program paths). Existing attempts on addressing this issue include those approaches based on constrained Horn clauses (in which the whole program is encoded as one constraint) and one preliminary attempt on caching and reusing partial solving results from the constraint solver. In this work, we propose\n                    <jats:sc>SEC<\/jats:sc>\n                    , which systematically computes the reward of concretizing a program path (for symbolic execution) and a variable (for constraint solving) and uses the reward as guide for integrating the two searches. We implemented\n                    <jats:sc>SEC<\/jats:sc>\n                    based on KLEE and evaluated it on a diverse set of programs. The results show that\n                    <jats:sc>SEC<\/jats:sc>\n                    is effective, i.e., achieving 15% more code coverage than the state-of-the-art baseline symbolic execution engines. Furthermore, we show that\n                    <jats:sc>SEC<\/jats:sc>\n                    can be readily combined with a state-of-the-art concolic testing engine to improve its performance\n                  <\/jats:p>","DOI":"10.1145\/3735552","type":"journal-article","created":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T12:23:51Z","timestamp":1747139031000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Integrating Path Selection for Symbolic Execution and Variable Selection for Constraint Solving"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6428-6739","authenticated-orcid":false,"given":"Shunkai","family":"Zhu","sequence":"first","affiliation":[{"name":"Zhejiang University, Hangzhou, 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-0001-7113-7635","authenticated-orcid":false,"given":"Jingyi","family":"Wang","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, 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\/0000-0002-4453-2274","authenticated-orcid":false,"given":"Peng","family":"Cheng","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]}],"member":"320","published-online":{"date-parts":[[2026,2,13]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.3390\/a15090302"},{"key":"e_1_3_3_3_2","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/1390630.1390662","volume-title":"Proceedings of the 2008 International Symposium on Software Testing and Analysis","author":"Artzi Shay","year":"2008","unstructured":"Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit Paradkar, and Michael D. Ernst. 2008. Finding bugs in dynamic web applications. In Proceedings of the 2008 International Symposium on Software Testing and Analysis, 261\u2013272."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_3_6_2","unstructured":"Mislav Balunovic Pavol Bielik and Martin Vechev. 2018. Learning to solve SMT formulas. In Proceedings of the 32nd International Conference on Neural Information Processing Systems."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_3_8_2","first-page":"193","volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201999) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS \u201999)","author":"Biere Armin","year":"1999","unstructured":"Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201999) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS \u201999). Springer, 193\u2013207."},{"key":"e_1_3_3_9_2","first-page":"351","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Boonstoppel Peter","year":"2008","unstructured":"Peter Boonstoppel, Cristian Cadar, and Dawson Engler. 2008. RWset: Attacking path explosion in constraint-based test generation. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 351\u2013366."},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1109\/SP.2019.00022","volume-title":"Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP)","author":"Brotzman Robert","year":"2019","unstructured":"Robert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan, and Mahmut Kandemir. 2019. CaSym: Cache aware symbolic execution for side channel detection and mitigation. In Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 505\u2013521."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397360"},{"key":"e_1_3_3_12_2","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","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 Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Vol. 8, 209\u2013224.","journal-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI)"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_3_15_2","first-page":"1244","volume-title":"Proceedings of the 40th International Conference on Software Engineering","author":"Cha Sooyoung","year":"2018","unstructured":"Sooyoung Cha, Seongjoon Hong, Junhee Lee, and Hakjoo Oh. 2018. Automatically generating search heuristics for concolic testing. In Proceedings of the 40th International Conference on Software Engineering, 1244\u20131254."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338964"},{"key":"e_1_3_3_17_2","first-page":"147","volume-title":"Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering","author":"Cha Sooyoung","year":"2020","unstructured":"Sooyoung Cha and Hakjoo Oh. 2020. Making symbolic execution promising by learning aggressive state-pruning strategy. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 147\u2013158."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_3_19_2","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1109\/SP.2017.40","volume-title":"Proceedings of the 2017 IEEE Symposium on Security and Privacy (SP)","author":"Chau Sze Yiu","year":"2017","unstructured":"Sze Yiu Chau, Omar Chowdhury, Endadul Hoque, Huangyi Ge, Aniket Kate, Cristina Nita-Rotaru, and Ninghui Li. 2017. Symcerts: Practical symbolic execution for exposing noncompliance in X. 509 certificate validation implementations. In Proceedings of the 2017 IEEE Symposium on Security and Privacy (SP). IEEE, 503\u2013520."},{"key":"e_1_3_3_20_2","volume-title":"Proceedings of the Network and Distributed Systems Security (NDSS) Symposium 2019","author":"Sze Yiu Chau","year":"2019","unstructured":"Sze Yiu Chau, Moosa Yahyazadeh, Omar Chowdhury, Aniket Kate, and Ninghui Li. 2019. Analyzing semantic correctness with symbolic execution: A case study on pkcs# 1 v1. 5 signature verification. In Proceedings of the Network and Distributed Systems Security (NDSS) Symposium 2019."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238218"},{"key":"e_1_3_3_22_2","volume-title":"Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP \u201918)","author":"Chen Junjie","year":"2018","unstructured":"Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, and Lu Zhang. 2018. Learning to accelerate symbolic execution via code transformation. In Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP \u201918). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","first-page":"1580","DOI":"10.1109\/SP40000.2020.00002","volume-title":"Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP)","author":"Chen Yaohui","year":"2020","unstructured":"Yaohui Chen, Peng Li, Jun Xu, Shengjian Guo, Rundong Zhou, Yulong Zhang, Tao Wei, and Long Lu. 2020. Savior: Towards bug-driven hybrid testing. In Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1580\u20131596."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Ganesh Vijay","year":"2007","unstructured":"Vijay Ganesh and David L. Dill. 2007. A decision procedure for bit-vectors and arrays. In Proceedings of the International Conference on Computer Aided Verification. Springer, 519\u2013531."},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1065010.1065036","volume-title":"Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Godefroid Patrice","year":"2005","unstructured":"Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed automated random testing. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, 213\u2013223."},{"key":"e_1_3_3_28_2","unstructured":"Patrice Godefroid Michael Y. Levin and David A. Molnar. 2008. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security (NDSS) Vol. 8 151\u2013166."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254112"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236028"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484813"},{"key":"e_1_3_3_32_2","first-page":"157","volume-title":"Proceedings of the International Conference on Theory and Applications of Satisfiability Testing","author":"Hoder Kry\u0161tof","year":"2012","unstructured":"Kry\u0161tof Hoder and Nikolaj Bj\u00f8rner. 2012. Generalized property directed reachability. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Springer, 157\u2013171."},{"key":"e_1_3_3_33_2","first-page":"247","volume-title":"Proceedings of the 18th International Symposium on Formal Methods (FM \u201912)","author":"Hojjat Hossein","year":"2012","unstructured":"Hossein Hojjat, Filip Kone\u010dn\u1ef3, Florent Garnier, Radu Iosif, Viktor Kuncak, and Philipp R\u00fcmmer. 2012. A verification toolkit for numerical transition systems: Tool paper. In Proceedings of the 18th International Symposium on Formal Methods (FM \u201912). Springer, 247\u2013251."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/2733572.2733574"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_3_36_2","first-page":"115","volume-title":"Proceedings of the 2020 35th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Kapus Timotej","year":"2020","unstructured":"Timotej Kapus, Frank Busse, and Cristian Cadar. 2020. Pending constraints in symbolic execution for better exploration and seeding. In Proceedings of the 2020 35th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 115\u2013126."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254088"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509553"},{"key":"e_1_3_3_41_2","first-page":"95","volume-title":"Proceedings of the International Static Analysis Symposium","author":"Ma Kin-Keung","year":"2011","unstructured":"Kin-Keung Ma, Khoo Yit Phang, Jeffrey S. Foster, and Michael Hicks. 2011. Directed symbolic execution. In Proceedings of the International Static Analysis Symposium. Springer, 95\u2013111."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200987"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.294"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_3_45_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/1858996.1859035","volume-title":"Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering","author":"P\u0103s\u0103reanu Corina S.","year":"2010","unstructured":"Corina S. P\u0103s\u0103reanu and Neha Rungta. 2010. Symbolic PathFinder: Symbolic execution of java bytecode. In Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering, 179\u2013180."},{"key":"e_1_3_3_46_2","first-page":"485","volume-title":"Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201915)","author":"Pedrosa Luis","year":"2015","unstructured":"Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. 2015. Analyzing protocol implementations for interoperability. In Proceedings of the 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201915), 485\u2013498."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993558"},{"key":"e_1_3_3_48_2","first-page":"181","volume-title":"Proceedings of the 29th USENIX Security Symposium (USENIX Security \u201920)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with \\(\\{\\) SymCC \\(\\}\\) : Don\u2019t interpret, compile! In Proceedings of the 29th USENIX Security Symposium (USENIX Security \u201920), 181\u2013198."},{"key":"e_1_3_3_49_2","volume-title":"Proceedings of the Network and Distributed System Security (NDSS)","author":"Poeplau Sebastian","year":"2021","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2021. SymQEMU: Compilation-based symbolic execution for binaries. In Proceedings of the Network and Distributed System Security (NDSS)."},{"key":"e_1_3_3_50_2","first-page":"326","volume-title":"Proceedings of the 25th International Symposium on Static Analysis (SAS \u201918)","author":"Prabhu Sumanth","year":"2018","unstructured":"Sumanth Prabhu, Kumar Madhukar, and R. Venkatesh. 2018. Efficiently learning safety proofs from appearance as well as behaviours. In Proceedings of the 25th International Symposium on Static Analysis (SAS \u201918). Springer, 326\u2013343."},{"key":"e_1_3_3_51_2","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-030-24258-9_24","volume-title":"Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT \u201919)","author":"Selsam Daniel","year":"2019","unstructured":"Daniel Selsam and Nikolaj Bj\u00f8rner. 2019. Guiding high-performance SAT solvers with unsat-core predictions. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT \u201919). Springer, 336\u2013353."},{"key":"e_1_3_3_52_2","unstructured":"Daniel Selsam Matthew Lamm Benedikt B\u00fcnz Percy Liang Leonardo de Moura and David L. Dill. 2018. Learning a SAT solver from single-bit supervision. arXiv:1802.03685. Retrieved from https:\/\/arxiv.org\/abs\/1802.03685"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_3_54_2","doi-asserted-by":"crossref","DOI":"10.14722\/ndss.2019.23530","article-title":"Neuro-symbolic execution: Augmenting symbolic execution with neural constraints","author":"Shen Shiqi","year":"2019","unstructured":"Shiqi Shen, Shweta Shinde, Soundarya Ramesh, Abhik Roychoudhury, and Prateek Saxena. 2019. Neuro-symbolic execution: Augmenting symbolic execution with neural constraints. In Proceedings of the Network and Distributed System Security (NDSS).","journal-title":"Proceedings of the Network and Distributed System Security (NDSS)"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_3_56_2","first-page":"480","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV \u201900)","author":"Ofer Shtrichman","year":"2000","unstructured":"Ofer Shtrichman. 2000. Tuning SAT checkers for bounded model checking. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV \u201900). Springer, 480\u2013494."},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3660817"},{"key":"e_1_3_3_58_2","unstructured":"Jialin Song Ravi Lanka Yisong Yue and Bistra Dilkina. 2020. A general large neighborhood search framework for solving integer linear programs. In Proceedings of the 34th International Conference on Neural Information Processing 20012\u201320023."},{"key":"e_1_3_3_59_2","first-page":"149","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Unno Hiroshi","year":"2015","unstructured":"Hiroshi Unno and Tachio Terauchi. 2015. Inferring simple solutions to recursion-free horn clauses via sampling. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 149\u2013163."},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996713"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2979701"},{"key":"e_1_3_3_62_2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1145\/3180155.3180177","volume-title":"Proceedings of the 40th International Conference on Software Engineering","author":"Wang Xinyu","year":"2018","unstructured":"Xinyu Wang, Jun Sun, Zhenbang Chen, Peixin Zhang, Jingyi Wang, and Yun Lin. 2018. Towards optimal concolic testing. In Proceedings of the 40th International Conference on Software Engineering, 291\u2013302."},{"key":"e_1_3_3_63_2","first-page":"662","volume-title":"Proceedings of the 2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER)","author":"Wu Jie","year":"2020","unstructured":"Jie Wu, Chengyu Zhang, and Geguang Pu. 2020. Reinforcement learning guided symbolic execution. In Proceedings of the 2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, 662\u2013663."},{"key":"e_1_3_3_64_2","first-page":"359","volume-title":"Proceedings of the 2009 IEEE\/IFIP International Conference on Dependable Systems & Networks. IEEE","author":"Xie Tao","year":"2009","unstructured":"Tao Xie, Nikolai Tillmann, Jonathan De Halleux, and Wolfram Schulte. 2009. Fitness-guided path exploration in dynamic symbolic execution. In Proceedings of the 2009 IEEE\/IFIP International Conference on Dependable Systems & Networks. IEEE, 359\u2013368."},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656443"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.11"},{"key":"e_1_3_3_68_2","first-page":"745","volume-title":"Proceedings of the 27th USENIX Security Symposium (USENIX Security \u201918)","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 Proceedings of the 27th USENIX Security Symposium (USENIX Security \u201918), 745\u2013761."},{"key":"e_1_3_3_69_2","first-page":"815","volume-title":"Proceedings of the 2018 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO)","author":"Zhang Rui","year":"2018","unstructured":"Rui Zhang, Calvin Deutschbein, Peng Huang, and Cynthia Sturton. 2018. End-to-end automated exploit generation for validating the security of processor designs. In Proceedings of the 2018 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO). IEEE, 815\u2013827."},{"key":"e_1_3_3_70_2","doi-asserted-by":"crossref","unstructured":"Wenjie Zhang Zeyu Sun Qihao Zhu Ge Li Shaowei Cai Yingfei Xiong and Lu Zhang. 2020. NLocalSAT: Boosting local search with solution prediction. arXiv:2001.09398. Retrieved from https:\/\/arxiv.org\/abs\/2001.09398","DOI":"10.24963\/ijcai.2020\/164"},{"key":"e_1_3_3_71_2","first-page":"846","volume-title":"Proceedings of the 2020 35th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Zhang Yufeng","year":"2020","unstructured":"Yufeng Zhang, Zhenbang Chen, Ziqi Shuai, Tianqi Zhang, Kenli Li, and Ji Wang. 2020. Multiplex symbolic execution: Exploring multiple paths by solving once. In Proceedings of the 2020 35th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 846\u2013857."},{"key":"e_1_3_3_72_2","first-page":"36","volume-title":"Proceedings of the 21st International Conference on Formal Methods and Software Engineering (ICFEM \u201919)","author":"Zhang Yueling","year":"2019","unstructured":"Yueling Zhang, Geguang Pu, and Min Zhang. 2019. Smtbcf: Efficient backbone computing for smt formulas. In Proceedings of the 21st International Conference on Formal Methods and Software Engineering (ICFEM \u201919). Springer, 36\u201351."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3735552","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:38:11Z","timestamp":1770993491000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3735552"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,13]]},"references-count":71,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3735552"],"URL":"https:\/\/doi.org\/10.1145\/3735552","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,13]]},"assertion":[{"value":"2024-06-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}