{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T18:35:01Z","timestamp":1773686101604,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T00:00:00Z","timestamp":1608508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Key R&D Program of China","award":["2017YFB1001802"],"award-info":[{"award-number":["2017YFB1001802"]}]},{"name":"NSFC","award":["61632015, 61625202, 61690203, 61532007"],"award-info":[{"award-number":["61632015, 61625202, 61690203, 61532007"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,12,21]]},"DOI":"10.1145\/3324884.3416645","type":"proceedings-article","created":{"date-parts":[[2021,1,27]],"date-time":"2021-01-27T23:38:56Z","timestamp":1611790736000},"page":"846-857","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Multiplex symbolic execution"],"prefix":"10.1145","author":[{"given":"Yufeng","family":"Zhang","sequence":"first","affiliation":[{"name":"Hunan University, Changsha, China"}]},{"given":"Zhenbang","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Ziqi","family":"Shuai","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Tianqi","family":"Zhang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Kenli","family":"Li","sequence":"additional","affiliation":[{"name":"Hunan University, Changsha, China"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2021,1,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2020. LibFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_2_1_3_1","unstructured":"Berkeley. 2020. SoftFloat 2b. http:\/\/www.jhauser.us\/arithmetic\/SoftFloat.html."},{"key":"e_1_3_2_1_4_1","volume-title":"Heuristics for Scalable Dynamic Test Generation. In 2008 23rd IEEE\/ACM International Conference on Automated Software Engineering. 443--446","author":"Burnim J.","unstructured":"J. Burnim and K. Sen. 2008. Heuristics for Scalable Dynamic Test Generation. In 2008 23rd IEEE\/ACM International Conference on Automated Software Engineering. 443--446."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation","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 (San Diego, California) (OSDI'08). USENIX Association, USA, 209--224."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180166"},{"key":"e_1_3_2_1_8_1","volume-title":"2018 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE). 408--418","author":"Cha S.","unstructured":"S. Cha, S. Lee, and H. Oh. 2018. Template-Guided Concolic Testing via Online Learning. In 2018 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE). 408--418."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338964"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831734"},{"key":"e_1_3_2_1_11_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337--340."},{"key":"e_1_3_2_1_12_1","volume-title":"Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers","author":"Dillig Isil","unstructured":"Isil Dillig, Thomas Dillig, and Alex Aiken. 2009. Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. In Computer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 233--247."},{"key":"e_1_3_2_1_13_1","volume-title":"A Fast Linear-Arithmetic Solver for DPLL(T)","author":"Dutertre Bruno","unstructured":"Bruno Dutertre and Leonardo de Moura. 2006. A Fast Linear-Arithmetic Solver for DPLL(T). In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 81--94."},{"key":"e_1_3_2_1_14_1","unstructured":"The Free Software Foundation. 2020. GNU Scientific Library. https:\/\/www.gnu.org\/software\/gsl\/."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification","author":"Ganesh Vijay","unstructured":"Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (Berlin, Germany) (CAV'07). Springer-Verlag, Berlin, Heidelberg, 519--531."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375607"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.220.4598.671"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254088"},{"key":"e_1_3_2_1_25_1","volume-title":"Linear Programming and Extensions","author":"Lasdon Leon S","unstructured":"Leon S Lasdon, Richard L Fox, and Margery W Ratner. 1963. Linear Programming and Extensions. Princeton University."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-74759-0_286"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509553"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_2_1_29_1","volume-title":"Jeffrey S Foster, and Michael Hicks.","author":"Ma Kin-Keung","year":"2011","unstructured":"Kin-Keung Ma, Khoo Yit Phang, Jeffrey S Foster, and Michael Hicks. 2011. Directed Symbolic Execution. In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 95--111."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1077276.1077279"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2014 (published 2015). Boolector 2.0 system description. Journal on Satisfiability Boolean Modeling and Computation 9 (2014 (published 2015)) 53--58.","DOI":"10.3233\/SAT190101"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1155\/2012\/674832"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2983966"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC'15)","author":"David","unstructured":"David A. Ramos and Dawson Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC'15). USENIX Association, USA, 49--64."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_19"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_14"},{"key":"e_1_3_2_1_40_1","volume-title":"Pasareanu","author":"Souza Matheus","year":"2011","unstructured":"Matheus Souza, Mateus Borges, Marcelo d'Amorim, and Corina S. Pasareanu. 2011. CORAL: Solving Complex Constraints for Symbolic PathFinder. In NASA Formal Methods."},{"key":"e_1_3_2_1_41_1","volume-title":"Pex-White Box Test Generation for .NET","author":"Tillmann Nikolai","unstructured":"Nikolai Tillmann and Jonathan de Halleux. 2008. Pex-White Box Test Generation for .NET. In Tests and Proofs, Bernhard Beckert and Reiner H\u00e4hnle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 134--153."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_2_1_43_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Wang Chao","unstructured":"Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. 2008. Peephole Partial Order Reduction. In Tools and Algorithms for the Construction and Analysis of Systems, C R Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 382--396."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180177"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(01)00190-2"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380419"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180227"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3122830"},{"key":"e_1_3_2_1_49_1","volume-title":"Speculative Symbolic Execution. In 2012 IEEE 23rd International Symposium on Software Reliability Engineering. 101--110","author":"Zhang Y.","unstructured":"Y. Zhang, Z. Chen, and J. Wang. 2012. Speculative Symbolic Execution. In 2012 IEEE 23rd International Symposium on Software Reliability Engineering. 101--110."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818833"}],"event":{"name":"ASE '20: 35th IEEE\/ACM International Conference on Automated Software Engineering","location":"Virtual Event Australia","acronym":"ASE '20","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416645","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3324884.3416645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:23Z","timestamp":1750193243000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416645"}},"subtitle":["exploring multiple paths by solving once"],"short-title":[],"issued":{"date-parts":[[2020,12,21]]},"references-count":49,"alternative-id":["10.1145\/3324884.3416645","10.1145\/3324884"],"URL":"https:\/\/doi.org\/10.1145\/3324884.3416645","relation":{},"subject":[],"published":{"date-parts":[[2020,12,21]]},"assertion":[{"value":"2021-01-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}