{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T13:33:17Z","timestamp":1790947997153,"version":"4.1.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>We propose Generative Type-Aware Mutation, an effective approach for testing SMT solvers. The key idea is to realize generation through the mutation of expressions rooted with parametric operators from the SMT-LIB specification. Generative Type-Aware Mutation is a hybrid of mutation-based and grammar-based fuzzing and features an infinite mutation space\u2014overcoming a major limitation of OpFuzz, the state-of-the-art fuzzer for SMT solvers. We have realized Generative Type-Aware Mutation in a practical SMT solver bug hunting tool, TypeFuzz. During our testing period with TypeFuzz, we reported over 237 bugs in the state-of-the-art SMT solvers Z3 and CVC4. Among these, 189 bugs were confirmed and 176 bugs were fixed. Most notably, we found 18 soundness bugs in CVC4\u2019s default mode alone. Several of them were two years latent (7\/18). CVC4 has been proved to be a very stable SMT solver and has resisted several fuzzing campaigns.<\/jats:p>","DOI":"10.1145\/3485529","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T15:18:28Z","timestamp":1634311108000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Generative type-aware mutation for testing SMT solvers"],"prefix":"10.1145","volume":"5","author":[{"given":"Jiwon","family":"Park","sequence":"first","affiliation":[{"name":"\u00c9cole Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominik","family":"Winterer","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chengyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/MobileSoft.2015.11"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23412"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2019. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org  Clark Barrett Pascal Fontaine and Cesare Tinelli. 2019. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_2_2_5_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In SMT \u201910.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In SMT \u201910."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855756"},{"key":"e_1_2_2_11_1","unstructured":"The International SMT Competition.. 2021. SMT-COMP. https:\/\/smt-comp.github.io\/2021\/  The International SMT Competition.. 2021. SMT-COMP. https:\/\/smt-comp.github.io\/2021\/"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_13_1","unstructured":"Rob DeLine and Rustan Leino. 2005. BoogiePL: A Typed Procedural Language for Checking Object-Oriented Programs.  Rob DeLine and Rustan Leino. 2005. BoogiePL: A Typed Procedural Language for Checking Object-Oriented Programs."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155573"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.94.0242"},{"key":"e_1_2_2_18_1","unstructured":"Gereon Kremer. 2021. pyDelta: delta debugging for SMT-LIB. https:\/\/github.com\/nafur\/pydelta  Gereon Kremer. 2021. pyDelta: delta debugging for SMT-LIB. https:\/\/github.com\/nafur\/pydelta"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_2_2_21_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT \u201917. 10.  Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT \u201917. 10."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2941681"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254104"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/3488766.3488804"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00081"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_2_2_31_1","unstructured":"Dominik Winterer Chengyu Zhang and Zhendong Su. 2021. yinyang: a fuzzer for SMT solvers. https:\/\/github.com\/testsmt\/yinyang  Dominik Winterer Chengyu Zhang and Zhendong Su. 2021. yinyang: a fuzzer for SMT solvers. https:\/\/github.com\/testsmt\/yinyang"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_33_1","unstructured":"Michal Zalewski. 2021. american fuzzy lop. https:\/\/lcamtuf.coredump.cx\/afl\/  Michal Zalewski. 2021. american fuzzy lop. https:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062379"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485529","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485529","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:18:40Z","timestamp":1750177120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485529"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":33,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485529"],"URL":"https:\/\/doi.org\/10.1145\/3485529","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}