{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T16:44:58Z","timestamp":1787330698986,"version":"build-2736575974"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"9","license":[{"start":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T00:00:00Z","timestamp":1787270400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["Grants 624B2067, 62572226, 62472215, and 62072194"],"award-info":[{"award-number":["Grants 624B2067, 62572226, 62472215, and 62072194"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004608","name":"Jiangsu Natural Science Foundation","doi-asserted-by":"crossref","award":["Grant BK20231402"],"award-info":[{"award-number":["Grant BK20231402"]}],"id":[{"id":"10.13039\/501100004608","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,9,30]]},"abstract":"<jats:p>\n                    Ensuring the correctness of Satisfiability Modulo Theory (SMT) solvers is critical, as undetected bugs in these solvers can lead to incorrect results in the many applications that depend on them. However, automatically testing SMT solvers remains challenging, largely due to the absence of reliable test oracles. To address this challenge, recent work has explored assignment-aided reassembling techniques, such as STORM and Diver, which generate satisfiable test formulas by recombining parts of existing formulas based on satisfying assignments. While these techniques have demonstrated effectiveness in practice, opportunities remain to further enhance the approaches. For example, they cannot generate unsatisfiable test formulas, which may restrict their ability to detect certain classes of soundness bugs. Therefore, this article introduces a novel fuzzing technique that enhances these methods building on the idea of assignment-aided reassembling. Specifically, our approach utilizes multiple satisfying assignments derived from seed formulas to guide the reassembly of sub-formulas, exploring divergent logical paths to synthesize new test cases. To further increase test diversity, we incorporate formula snippets generated from scratch. In addition, we extend the approach to support the generation of unsatisfiable test formulas by using unsatisfiable cores extracted from unsatisfiable seed formulas. We have implemented this approach in a practical tool,\n                    <jats:sc>Octopus<\/jats:sc>\n                    , designed to test SMT solvers more comprehensively. We applied\n                    <jats:sc>Octopus<\/jats:sc>\n                    to leading SMT solvers, including Z3 and cvc5, and reported 13 bugs to their issue trackers. Among these, 11 bugs have been confirmed by the developers, and nine have been fixed. Our experiments also show that\n                    <jats:sc>Octopus<\/jats:sc>\n                    achieves higher code coverage compared to existing SMT fuzzers.\n                  <\/jats:p>","DOI":"10.1145\/3788862","type":"journal-article","created":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T14:49:24Z","timestamp":1768834164000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Oracle-Guided SMT Solver Validation via Synthesizing Diverse Formulas with Multiple Assignments"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5617-2205","authenticated-orcid":false,"given":"Maolin","family":"Sun","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1153-2013","authenticated-orcid":false,"given":"Yibiao","family":"Yang","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9932-7315","authenticated-orcid":false,"given":"Jiangchang","family":"Wu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5666-2158","authenticated-orcid":false,"given":"Qingyang","family":"Li","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7370-6421","authenticated-orcid":false,"given":"Zeyu","family":"Lu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4645-2526","authenticated-orcid":false,"given":"Yuming","family":"Zhou","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,21]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Daniel Larraz. 2025. The International SMT Competition. Retrieved from https:\/\/github.com\/cvc5\/cvc5"},{"key":"e_1_3_3_3_2","unstructured":"GNU GCC. 2021. Using the GNU Compiler Collection\u2014GCov. Retrieved from https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/Gcov.html"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23412"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_3_7_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2025. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved from https:\/\/smtlib.cs.uiowa.edu\/"},{"key":"e_1_3_3_8_2","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."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428209"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_3_12_2","unstructured":"Martin Brain. 2023. Random Solutions. Retrieved from https:\/\/github.com\/cvc5\/cvc5\/discussions\/9581#discussioncomment-5395757"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3560435"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_3_15_2","first-page":"209","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201908)","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 \u201908). Richard Draves and Robbert van Renesse (Eds.), USENIX Association, 209\u2013224. Retrieved from http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884878"},{"key":"e_1_3_3_17_2","unstructured":"Tsong Yueh Chen S. C. Cheung and Siu-Ming Yiu. 2020. Metamorphic testing: A new approach for generating next test cases. arXiv:2002.12543. Retrieved from https:\/\/arxiv.org\/abs\/2002.12543"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3143561"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_20_2","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS \u201908)","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security Symposium (NDSS \u201908). The Internet Society. Retrieved from https:\/\/www.ndss-symposium.org\/ndss2008\/automated-whitebox-fuzz-testing\/"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23263"},{"key":"e_1_3_3_22_2","unstructured":"Heqing Huang. 2023. CVE-2020-19725. Retrieved November 5 2023 from https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2020-19725#"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSESS.2013.6615365"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00187"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_11"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2011.6115306"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177730491"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_3_30_2","first-page":"867","volume-title":"Proceedings of the 20th International Conference on Software Engineering and Knowledge Engineering (SEKE \u2019 08)","author":"Murphy Christian","year":"2008","unstructured":"Christian Murphy, Gail E. Kaiser, Lifeng Hu, and Leon Wu. 2008. Properties of machine learning applications for use in metamorphic testing. In Proceedings of the 20th International Conference on Software Engineering and Knowledge Engineering (SEKE \u2019 08). Knowledge Systems Institute Graduate School, 867\u2013872."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2941681"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_6"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2532875"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"e_1_3_3_38_2","unstructured":"SMT-COMP. 2021. The International SMT Competition. Retrieved from https:\/\/smt-comp.github.io\/2021\/index.html"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00180"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00018"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763093"},{"key":"e_1_3_3_43_2","unstructured":"Maolin Sun Yibiao Yang and Yuming Zhou. 2025. Boosting skeleton-driven SMT solver fuzzing by leveraging LLM to produce formula generators. arXiv:2508.20340. Retrieved from https:\/\/arxiv.org\/abs\/2508.20340"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3119186"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-016-5544-6"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468596"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689795"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2009.26"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00018"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616340"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707271"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464803"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468540"},{"key":"e_1_3_3_56_2","unstructured":"Michal Zalewski. 2014. American Fuzzy Lop. Retrieved from http:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416645"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3168373"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.437"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3788862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T16:21:31Z","timestamp":1787329291000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3788862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,21]]},"references-count":58,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2026,9,30]]}},"alternative-id":["10.1145\/3788862"],"URL":"https:\/\/doi.org\/10.1145\/3788862","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,21]]},"assertion":[{"value":"2024-11-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-08-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}