{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T04:08:56Z","timestamp":1750392536955,"version":"3.41.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2022YFB4501903"],"award-info":[{"award-number":["2022YFB4501903"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["62172429 & 62032024"],"award-info":[{"award-number":["62172429 & 62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,19]]},"abstract":"<jats:p>Floating-point constraint solving is challenging due to the complex representation and non-linear computations. Search-based constraint solving provides an effective method for solving floating-point constraints. In this paper, we propose QSF to improve the efficiency of search-based solving for floating-point constraints. The key idea of QSF is to model the floating-point constraint solving problem as a multi-objective optimization problem. Specifically, QSF considers both the number of unsatisfied constraints and the sum of the violation degrees of unsatisfied constraints as the objectives for search-based optimization. Besides, we propose a new evolutionary algorithm in which the mutation operators are specially designed for floating-point numbers, aiming to solve the multi-objective problem more efficiently. We have implemented QSF and conducted extensive experiments on both the SMT-COMP benchmark and the benchmark from real-world floating-point programs. The results demonstrate that compared to SOTA floating-point solvers, QSF achieved an average speedup of 15.72X under a 60-second timeout and an impressive 87.48X under a 600-second timeout on the first benchmark. Similarly, on the second benchmark, QSF delivered an average speedup of 22.44X and 29.23X, respectively, under the two timeout configurations. Furthermore, QSF has also enhanced the performance of symbolic execution for floating-point programs.<\/jats:p>","DOI":"10.1145\/3715739","type":"journal-article","created":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:15:34Z","timestamp":1750346134000},"page":"511-532","source":"Crossref","is-referenced-by-count":0,"title":["QSF: Multi-objective Optimization Based Efficient Solving for Floating-Point Constraints"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6177-9164","authenticated-orcid":false,"given":"Xu","family":"Yang","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\/0000-0002-8033-7943","authenticated-orcid":false,"given":"Wei","family":"Dong","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"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":[[2025,6,19]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"1985. IEEE standard for binary floating-point arithmetic - IEEE standard 754-1985. Beuth."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020281327116"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-023-00423-0"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Earl T. Barr Thanh Vo Vu Le and Zhendong Su. 2013. Automatic detection of floating-point exceptions. 549\u2013560. https:\/\/doi.org\/10.1145\/2429069.2429133 10.1145\/2429069.2429133","DOI":"10.1145\/2429069.2429133"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK). 13, 14."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 35th Conference on Design Automation, Moscone center","author":"Barrett Clark W.","year":"1998","unstructured":"Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. 1998. A Decision Procedure for Bit-Vector Arithmetic. In Proceedings of the 35th Conference on Design Automation, Moscone center, San Francico, California, USA, June 15-19, 1998, Basant R. Chawla, Randal E. Bryant, and Jan M. Rabaey (Eds.). ACM Press, 522\u2013527. https:\/\/doi.org\/10.1145\/277044.277186 10.1145\/277044.277186"},{"key":"e_1_2_1_8_1","volume-title":"Proc. ACM Program. Lang., 7, POPL","author":"Bembenek Aaron","year":"2023","unstructured":"Aaron Bembenek, Michael Greenberg, and Stephen Chong. 2023. From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems. Proc. ACM Program. Lang., 7, POPL (2023), 185\u2013217. https:\/\/doi.org\/10.1145\/3571200 10.1145\/3571200"},{"key":"e_1_2_1_9_1","volume-title":"FMCAD 2017","author":"Khadra M. Ammar Ben","year":"2017","unstructured":"M. Ammar Ben Khadra, Dominik Stoffel, and Wolfgang Kunz. 2017. goSAT: Floating-point satisfiability as global optimization. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 11\u201314. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102235 10.23919\/FMCAD.2017.8102235"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1214\/ss"},{"key":"e_1_2_1_11_1","volume-title":"Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.) (Frontiers in Artificial Intelligence and Applications","unstructured":"2009. Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.) (Frontiers in Artificial Intelligence and Applications, Vol. 185). IOS Press. isbn:978-1-58603-929-5"},{"key":"e_1_2_1_12_1","volume-title":"FMCAD 2008","author":"Bofill Miquel","year":"2008","unstructured":"Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodr\u00edguez-Carbonell, and Albert Rubio. 2008. A Write-Based Solver for SAT Modulo the Theory of Arrays. In Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008, Alessandro Cimatti and Robert B. Jones (Eds.). IEEE, 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2008.ECP.18 10.1109\/FMCAD.2008.ECP.18"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_5"},{"key":"e_1_2_1_15_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, Richard Draves and Robbert van Renesse (Eds.). USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01442131"},{"key":"e_1_2_1_17_1","volume-title":"Proc. ACM Softw. Eng., 1, FSE","author":"Chen Tao","year":"2024","unstructured":"Tao Chen and Miqing Li. 2024. Adapting Multi-objectivized Software Configuration Tuning. Proc. ACM Softw. Eng., 1, FSE (2024), 539\u2013561. https:\/\/doi.org\/10.1145\/3643751 10.1145\/3643751"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_2_1_19_1","volume-title":"The Complexity of Theorem-Proving Procedures (1 ed.)","author":"Cook Stephen A.","unstructured":"Stephen A. Cook. 2023. The Complexity of Theorem-Proving Procedures (1 ed.). Association for Computing Machinery, New York, NY, USA. 143\u2013152. isbn:9798400707797"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4324\/9781315693361"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/4235.996017"},{"key":"e_1_2_1_23_1","volume-title":"Genetic and Evolutionary Computation Conference, GECCO 2007","author":"Deb Kalyanmoy","year":"2007","unstructured":"Kalyanmoy Deb, Karthik Sindhya, and Tatsuya Okabe. 2007. Self-adaptive simulated binary crossover for real-parameter optimization. In Genetic and Evolutionary Computation Conference, GECCO 2007, Proceedings, London, England, UK, July 7-11, 2007, Hod Lipson (Ed.). ACM, 1187\u20131194. https:\/\/doi.org\/10.1145\/1276958.1277190 10.1145\/1276958.1277190"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00234-2_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"A. E. Eiben and J. E. Smith. 2015. What Is an Evolutionary Algorithm? Springer Berlin Heidelberg Berlin Heidelberg. 25\u201348. isbn:978-3-662-44874-8 https:\/\/doi.org\/10.1007\/978-3-662-44874-8_3 10.1007\/978-3-662-44874-8_3","DOI":"10.1007\/978-3-662-44874-8_3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1568-4946(02)00021-2"},{"key":"e_1_2_1_27_1","volume-title":"27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","author":"Fan Hongyu","year":"2022","unstructured":"Hongyu Fan, Weiting Liu, and Fei He. 2022. Interference relation-guided SMT solving for multi-threaded program verification. In PPoPP \u201922: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2 - 6, 2022, Jaejin Lee, Kunal Agrawal, and Michael F. Spear (Eds.). ACM, 163\u2013176. https:\/\/doi.org\/10.1145\/3503221.3508424 10.1145\/3503221.3508424"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1162\/EVCO.2008.16.3.355"},{"key":"e_1_2_1_29_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science","volume":"209","author":"Fu Zhoulai","year":"2016","unstructured":"Zhoulai Fu and Zhendong Su. 2016. XSat: A Fast Floating-Point Satisfiability Solver. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Swarat Chaudhuri and Azadeh Farzan (Eds.) (Lecture Notes in Computer Science, Vol. 9780). Springer, 187\u2013209. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11 10.1007\/978-3-319-41540-6_11"},{"key":"e_1_2_1_30_1","volume-title":"VSTTE 2020, and 13th International Workshop, NSV 2020","author":"Gadelha Mikhail R.","year":"2020","unstructured":"Mikhail R. Gadelha, Lucas C. Cordeiro, and Denis A. Nicole. 2020. An Efficient Floating-Point Bit-Blasting API for Verifying C Programs. In Software Verification - 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers, Maria Christakis, Nadia Polikarpova, Parasara Sridhar Duggirala, and Peter Schrammel (Eds.) (Lecture Notes in Computer Science, Vol. 12549). Springer, 178\u2013195. https:\/\/doi.org\/10.1007\/978-3-030-63618-0_11 10.1007\/978-3-030-63618-0_11"},{"key":"e_1_2_1_31_1","unstructured":"Mark Galassi Jim Davies James Theiler Brian Gough Gerard Jungman Patrick Alken Michael Booth Fabrice Rossi and Rhys Ulerich. 2002. GNU scientific library. Network Theory Limited Godalming."},{"key":"e_1_2_1_32_1","volume-title":"USA","volume":"214","author":"Gao Sicun","year":"2013","unstructured":"Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Maria Paola Bonacina (Ed.) (Lecture Notes in Computer Science, Vol. 7898). Springer, 208\u2013214. https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14 10.1007\/978-3-642-38574-2_14"},{"key":"e_1_2_1_33_1","unstructured":"Steven G. Johnson. 2007. The NLopt nonlinear-optimization package. https:\/\/github.com\/stevengj\/nlopt"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10957-006-9101-0"},{"key":"e_1_2_1_35_1","first-page":"94720","article-title":"IEEE standard 754 for binary floating-point arithmetic","volume":"754","author":"Kahan William","year":"1996","unstructured":"William Kahan. 1996. IEEE standard 754 for binary floating-point arithmetic. Lecture Notes on the Status of IEEE, 754, 94720-1776 (1996), 11.","journal-title":"Lecture Notes on the Status of IEEE"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of International Conference on Neural Networks (ICNN\u201995)","author":"Kennedy James","year":"1995","unstructured":"James Kennedy and Russell Eberhart. 1995. Particle swarm optimization. In Proceedings of International Conference on Neural Networks (ICNN\u201995), Perth, WA, Australia, November 27 - December 1, 1995. IEEE, 1942\u20131948. https:\/\/doi.org\/10.1109\/ICNN.1995.488968 10.1109\/ICNN.1995.488968"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30217-9_75"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5120\/ijca2017913370"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-50497-0"},{"key":"e_1_2_1_40_1","volume-title":"ICTSS 2010, Natal, Brazil, November 8-10, 2010. Proceedings, Alexandre Petrenko, Adenilso da Silva Sim\u00e3o, and Jos\u00e9 Carlos Maldonado (Eds.) (Lecture Notes in Computer Science","volume":"157","author":"Lakhotia Kiran","year":"2010","unstructured":"Kiran Lakhotia, Nikolai Tillmann, Mark Harman, and Jonathan de Halleux. 2010. FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. In Testing Software and Systems - 22nd IFIP WG 6.1 International Conference, ICTSS 2010, Natal, Brazil, November 8-10, 2010. Proceedings, Alexandre Petrenko, Adenilso da Silva Sim\u00e3o, and Jos\u00e9 Carlos Maldonado (Eds.) (Lecture Notes in Computer Science, Vol. 6435). Springer, 142\u2013157. https:\/\/doi.org\/10.1007\/978-3-642-16573-3_11 10.1007\/978-3-642-16573-3_11"},{"key":"e_1_2_1_41_1","volume-title":"LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004)","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA. IEEE Computer Society, 75\u201388. https:\/\/doi.org\/10.1109\/CGO.2004.1281665 10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.proeng.2012.01.172"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2019","author":"Liew Daniel","year":"2019","unstructured":"Daniel Liew, Cristian Cadar, Alastair F. Donaldson, and J. Ryan Stinnett. 2019. Just fuzz it: solving floating-point constraints using coverage-guided fuzzing. In Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2019, Tallinn, Estonia, August 26-30, 2019, Marlon Dumas, Dietmar Pfahl, Sven Apel, and Alessandra Russo (Eds.). ACM, 521\u2013532. https:\/\/doi.org\/10.1145\/3338906.3338921 10.1145\/3338906.3338921"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10479-021-04033-Z"},{"key":"e_1_2_1_45_1","volume-title":"Real Behavior of Floating Point Numbers. In The SMT Workshop","author":"Marre Bruno","year":"2017","unstructured":"Bruno Marre, Fran\u00e7ois Bobot, and Zakaria Chihani. 2017. Real Behavior of Floating Point Numbers. In The SMT Workshop. Heidelberg, Germany. https:\/\/cea.hal.science\/cea-01795760"},{"key":"e_1_2_1_46_1","volume-title":"7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, Toby Walsh (Ed.) (Lecture Notes in Computer Science","volume":"538","author":"Michel Claude","year":"2001","unstructured":"Claude Michel, Michel Rueher, and Yahia Lebbah. 2001. Solving Constraints over Floating-Point Numbers. In Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, Toby Walsh (Ed.) (Lecture Notes in Computer Science, Vol. 2239). Springer, 524\u2013538. https:\/\/doi.org\/10.1007\/3-540-45578-7_36 10.1007\/3-540-45578-7_36"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2023","author":"Mikek Benjamin","year":"2023","unstructured":"Benjamin Mikek and Qirun Zhang. 2023. Speeding up SMT Solving via Compiler Optimization. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2023, San Francisco, CA, USA, December 3-9, 2023, Satish Chandra, Kelly Blincoe, and Paolo Tonella (Eds.). ACM, 1177\u20131189. https:\/\/doi.org\/10.1145\/3611643.3616357 10.1145\/3611643.3616357"},{"key":"e_1_2_1_48_1","volume-title":"CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, Constantin Enea and Akash Lal (Eds.) (Lecture Notes in Computer Science","volume":"17","author":"Niemetz Aina","year":"2023","unstructured":"Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II, Constantin Enea and Akash Lal (Eds.) (Lecture Notes in Computer Science, Vol. 13965). Springer, 3\u201317."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1162\/evco.1998.6.3.231"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10515-014-0154-2"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-017-0270-2"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4145-2_5"},{"key":"e_1_2_1_54_1","volume-title":"VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, Kenneth L. McMillan and Xavier Rival (Eds.) (Lecture Notes in Computer Science","volume":"356","author":"Romano Anthony","year":"2014","unstructured":"Anthony Romano. 2014. Practical Floating-Point Tests with Integer Code. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, Kenneth L. McMillan and Xavier Rival (Eds.) (Lecture Notes in Computer Science, Vol. 8318). Springer, 337\u2013356. https:\/\/doi.org\/10.1007\/978-3-642-54013-4_19 10.1007\/978-3-642-54013-4_19"},{"key":"e_1_2_1_55_1","volume-title":"Proc. ACM Softw. Eng., 1, FSE","author":"Shuai Ziqi","year":"2024","unstructured":"Ziqi Shuai, Zhenbang Chen, Kelin Ma, Kunlin Liu, Yufeng Zhang, Jun Sun, and Ji Wang. 2024. Partial Solution Based Constraint Solving Cache in Symbolic Execution. Proc. ACM Softw. Eng., 1, FSE (2024), 2493\u20132514. https:\/\/doi.org\/10.1145\/3660817 10.1145\/3660817"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","unstructured":"S.N. Sivanandam and S.N. Deepa. 2008. Genetic Algorithms. Springer Berlin Heidelberg Berlin Heidelberg. 15\u201337. isbn:978-3-540-73190-0 https:\/\/doi.org\/10.1007\/978-3-540-73190-0_2 10.1007\/978-3-540-73190-0_2","DOI":"10.1007\/978-3-540-73190-0_2"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"},{"key":"e_1_2_1_58_1","volume-title":"SMT-Based Theorem Verification for Testing-Based Formal Verification. In ICSCA 2021, 10th International Conference on Software and Computer Applications","author":"Sugai Kenta","year":"2021","unstructured":"Kenta Sugai, Hiroshi Hosobe, and Shaoying Liu. 2021. SMT-Based Theorem Verification for Testing-Based Formal Verification. In ICSCA 2021, 10th International Conference on Software and Computer Applications, Kuala Lumpur, Malaysia, February 23-26, 2021. ACM, 251\u2013257. https:\/\/doi.org\/10.1145\/3457784.3457823 10.1145\/3457784.3457823"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 3rd International Conference on Genetic Algorithms","author":"Syswerda Gilbert","year":"1989","unstructured":"Gilbert Syswerda. 1989. Uniform Crossover in Genetic Algorithms. In Proceedings of the 3rd International Conference on Genetic Algorithms, George Mason University, Fairfax, Virginia, USA, June 1989, J. David Schaffer (Ed.). Morgan Kaufmann, 2\u20139."},{"key":"e_1_2_1_60_1","volume-title":"Pex\u2013White Box Test Generation for .NET","author":"Tillmann Nikolai","unstructured":"Nikolai Tillmann and Jonathan de Halleux. 2008. Pex\u2013White Box Test Generation for .NET. In Tests and Proofs, Bernhard Beckert and Reiner H\u00e4hnle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 134\u2013153. isbn:978-3-540-79124-9"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1002\/MALQ.200610007"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2023.3252612"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2024.112242"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2021.3118593"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2007.892759"},{"key":"e_1_2_1_66_1","volume-title":"35th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2020","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 35th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, September 21-25, 2020. IEEE, 846\u2013857. https:\/\/doi.org\/10.1145\/3324884.3416645 10.1145\/3324884.3416645"},{"key":"e_1_2_1_67_1","volume-title":"Proc. ACM Softw. Eng., 1, FSE","author":"Zhou Shasha","year":"2024","unstructured":"Shasha Zhou, Mingyu Huang, Yanan Sun, and Ke Li. 2024. Evolutionary Multi-objective Optimization for Contextual Adversarial Example Generation. Proc. ACM Softw. Eng., 1, FSE (2024), 2285\u20132308. https:\/\/doi.org\/10.1145\/3660808 10.1145\/3660808"},{"key":"e_1_2_1_68_1","volume-title":"CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, J. Christopher Beck (Ed.) (Lecture Notes in Computer Science","volume":"722","author":"Zitoun Heytem","year":"2017","unstructured":"Heytem Zitoun, Claude Michel, Michel Rueher, and Laurent Michel. 2017. Search Strategies for Floating Point Constraint Systems. In Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, J. Christopher Beck (Ed.) (Lecture Notes in Computer Science, Vol. 10416). Springer, 707\u2013722. https:\/\/doi.org\/10.1007\/978-3-319-66158-2_45 10.1007\/978-3-319-66158-2_45"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3715739","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:34:34Z","timestamp":1750347274000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715739"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,19]]},"references-count":68,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2025,6,19]]}},"alternative-id":["10.1145\/3715739"],"URL":"https:\/\/doi.org\/10.1145\/3715739","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,19]]}}}