{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T18:57:16Z","timestamp":1782845836407,"version":"3.54.5"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T00:00:00Z","timestamp":1782777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"the National Key Research and Development Program of China","award":["2023YFB3307500"],"award-info":[{"award-number":["2023YFB3307500"]}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62202025"],"award-info":[{"award-number":["62202025"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62522201"],"award-info":[{"award-number":["62522201"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"the Young Elite Scientist Sponsorship Program by CAST","award":["YESS20230566"],"award-info":[{"award-number":["YESS20230566"]}]},{"name":"Beijing Natural Science Foundation","award":["L241050"],"award-info":[{"award-number":["L241050"]}]},{"name":"CCF-Huawei Populus Grove Fund","award":["CCF-HuaweiFM2024005"],"award-info":[{"award-number":["CCF-HuaweiFM2024005"]}]},{"name":"the Fundamental Research Fund Project of Beihang University","award":["None"],"award-info":[{"award-number":["None"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>\n                    Satisfiability Modulo Theories (SMT) is a fundamental technique underpinning a wide range of applications in software engineering and testing. Among various SMT theories, the theory of floating-point plays a crucial role in practical software systems, yet reasoning about floating-point constraints remains challenging. Although existing SMT solvers are capable of producing single solutions, many applications, particularly in software testing and verification, require diverse sets of solutions to adequately exercise program behaviors. While achieving high diversity is essential for exploring system behaviors, it is also important to limit the number of generated solutions, as overly large solution sets can considerably increase testing time and resource consumption, thereby diminishing efficiency. In this work, we propose\n                    <jats:italic toggle=\"yes\">DiverFPS<\/jats:italic>\n                    , a novel floating-point SMT sampler designed to generate small solution sets that achieve high target abstract syntax tree (AST)-coverage, which is commonly regarded as the standard metric for assessing solution diversity in the SMT sampling domain.\n                    <jats:italic toggle=\"yes\">DiverFPS<\/jats:italic>\n                    operates in two stages: an exploration stage that aims to achieve the target AST-coverage as fully as possible, and a pruning stage that prunes redundant solutions while preserving the target AST-coverage. We further introduce three novel techniques, namely solution-driven restart strategy, context-aware encoding technology, and coverage-driven pruning strategy, which enhance the performance of\n                    <jats:italic toggle=\"yes\">DiverFPS<\/jats:italic>\n                    . Extensive experiments on publicly available SMT-LIB benchmarks for QF_FP and QF_BVFP logics demonstrate that\n                    <jats:italic toggle=\"yes\">DiverFPS<\/jats:italic>\n                    outperforms state-of-the-art SMT samplers. It successfully achieves the target AST-coverage on a larger number of benchmarks, which existing samplers fail to reach, while producing solution sets that are up to 92.9These results demonstrate that\n                    <jats:italic toggle=\"yes\">DiverFPS<\/jats:italic>\n                    is a high-performing sampler for floating-point SMT sampling.\n                  <\/jats:p>","DOI":"10.1145\/3797081","type":"journal-article","created":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T17:06:14Z","timestamp":1782839174000},"page":"1172-1195","source":"Crossref","is-referenced-by-count":0,"title":["DiverFPS: Generating Diverse Solutions for Floating-Point SMT Formulas"],"prefix":"10.1145","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-2040-9428","authenticated-orcid":false,"given":"Shuangyu","family":"Lyu","sequence":"first","affiliation":[{"name":"Beihang University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5028-1064","authenticated-orcid":false,"given":"Chuan","family":"Luo","sequence":"additional","affiliation":[{"name":"Beihang University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0520-6231","authenticated-orcid":false,"given":"Ruizhi","family":"Shi","sequence":"additional","affiliation":[{"name":"Beihang University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7083-2038","authenticated-orcid":false,"given":"Zhuo","family":"Su","sequence":"additional","affiliation":[{"name":"Beihang University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3473-9703","authenticated-orcid":false,"given":"Chunming","family":"Hu","sequence":"additional","affiliation":[{"name":"Beihang University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,30]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"1992. Patriot Missile Defense: Software Problem Led to System Failure at Dhahran Saudi Arabia. Technical Report GAO\/IMTEC-92-26. http:\/\/klabs.org\/richcontent\/Reports\/Failure_Reports\/patriot\/patriot_gao_145960.pdf"},{"key":"e_1_2_1_2_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. https:\/\/smt-lib.org\/"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11402763_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/GEFS.2013.6601055"},{"key":"e_1_2_1_6_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08)","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 (OSDI'08). USENIX Association, 209-224. https:\/\/api.semanticscholar.org\/CorpusID:2520229"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST62969.2025.10989031"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593097"},{"key":"e_1_2_1_12_1","unstructured":"Jianfeng Chen Xipeng Shen and Tim Menzies. 2020. Building Very Small Test Suites (with Snap). arXiv:1905.05358 [cs.SE] https:\/\/arxiv.org\/abs\/1905.05358"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729279"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240848"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894251"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 14th USENIX Conference on Offensive Technologies (WOOT'20)","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi, Dominik Maier, Heiko Ei\u00dffeldt, and Marc Heuse. 2020. AFL++: combining incremental steps of fuzzing research. In Proceedings of the 14th USENIX Conference on Offensive Technologies (WOOT'20). USENIX Association, Article 10, 1 pages. https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_1_23_1","volume-title":"Automated Whitebox Fuzz Testing. In Network and Distributed System Security Symposium. https:\/\/api.semanticscholar.org\/CorpusID:1296783","author":"Godefroid Patrice","unstructured":"Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Network and Distributed System Security Symposium. https:\/\/api.semanticscholar.org\/CorpusID:1296783"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/152388.152391"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3382025.3414951"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00063"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i13.26978"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3289073"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3638246"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102235"},{"key":"e_1_2_1_35_1","volume-title":"Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation","author":"Kitchen Nathan","year":"2010","unstructured":"Nathan Kitchen. 2010. Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. University of California, Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2010\/EECS-2010-165.html"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_38_1","unstructured":"LibFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.004"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416629"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2014.2346196"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3688836"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468622"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549155"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2946563"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_23"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2023"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-35510-4_4"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377813.3381346"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_6"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 29th USENIX Conference on Security Symposium (SEC'20)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SYMCC: don't interpret, compile!. In Proceedings of the 29th USENIX Conference on Security Symposium (SEC'20). USENIX Association, 18 pages. https: \/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/poeplau"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2693208.2693242"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/QRS54544.2021.00042"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2018.00018"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3712186"},{"key":"e_1_2_1_59_1","volume-title":"Meel","author":"Shaw Arijit","year":"2024","unstructured":"Arijit Shaw and Kuldeep S. Meel. 2024. CSB: A Counting and Sampling Tool for Bit-vectors. In Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024 (CEUR Workshop Proceedings, Vol. 3725), Giles Reger and Yoni Zohar (Eds.). CEUR-WS.org, 36-43. https:\/\/api.semanticscholar.org\/CorpusID:271333193"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524842"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.3102\/10769986025002101"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00521-016-2599-7"},{"key":"e_1_2_1_63_1","unstructured":"Michal Zalewski. [n. d.]. Technical whitepaper for afl-fuzz. http:\/\/lcamtuf.coredump.cx\/afl\/technical_details.txt Received 2025-09-12; accepted 2025-12-22"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3797081","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T17:58:10Z","timestamp":1782842290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3797081"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,30]]},"references-count":63,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3797081"],"URL":"https:\/\/doi.org\/10.1145\/3797081","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,30]]}}}