{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:00Z","timestamp":1780994700551,"version":"3.54.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"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":[[2024,10,8]]},"abstract":"<jats:p>\n                    One of the primary challenges in software testing is generating high-quality test inputs and obtaining corresponding test oracles. This paper introduces a novel methodology to mitigate this challenge in testing program verifiers by employing SMT (Satisfiability Modulo Theories) formulas as a universal test case generator. The key idea is to transform SMT formulas into programs and link the satisfiability of the formulas with the safety property of the programs, allowing the satisfiability of the formulas to act as a test oracle for program verifiers. This method was implemented as a framework named\n                    <jats:italic toggle=\"yes\">SMT2Test<\/jats:italic>\n                    , which enables the transformation of SMT formulas into Dafny and C programs. An intermediate representation was designed to augment the flexibility of this framework, streamlining the transformation for other programming languages and fostering modular transformation strategies. We evaluated the effectiveness of\n                    <jats:italic toggle=\"yes\">SMT2Test<\/jats:italic>\n                    by finding defects in two program verifiers: the Dafny verifier and CPAchecker. Utilizing the\n                    <jats:italic toggle=\"yes\">SMT2Test<\/jats:italic>\n                    framework with the SMT formulas from the SMT competition and SMT solver fuzzers, we discovered and reported a total of 14 previously unknown defects in these program verifiers that were not found by previous methods. After reporting, all of them have been confirmed, and 6 defects have been fixed. These findings show the effectiveness of our method and imply its potential application in testing other programming language infrastructures.\n                  <\/jats:p>","DOI":"10.1145\/3689719","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"222-245","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["SMT2Test: From SMT Formulas to Effective Test Cases"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7285-289X","authenticated-orcid":false,"given":"Chengyu","family":"Zhang","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2014.2372785"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5571-3_12"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_1_11_1","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs.","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs.. In OSDI, Vol. 8. 209\u2013224.","journal-title":"OSDI"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213848"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/qrs54544.2021.00032"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_1_24_1","first-page":"99","article-title":"Storage systems are distributed systems (so verify them that way!)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage systems are distributed systems (so verify them that way!). In OSDI. 99\u2013115.","journal-title":"OSDI"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624007.3624056"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_13"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ase.2017.8115669"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/c-m.1978.218139"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814319"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_3_1_39_1","first-page":"218","article-title":"Exception Safety for C#.","volume":"4","author":"Leino K Rustan M","year":"2004","unstructured":"K Rustan M Leino and Wolfram Schulte. 2004. Exception Safety for C#.. In SEFM, Vol. 4. 218\u2013227.","journal-title":"SEFM,"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_37"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011044"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616357"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993513"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/2161638"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380250705"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863538"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Dominik Winterer Chengyu Zhang and Zhendong Su. 2020b. Validating SMT solvers via semantic fusion. In PLDI. 718\u2013730. https:\/\/doi.org\/10.1145\/3385412.3385985 10.1145\/3385412.3385985","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.1993532"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464803"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468540"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338932"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Chengyu Zhang and Zhendong Su. 2024. Artifact: SMT2Test: From SMT Formulas to Effective Test Cases. https:\/\/doi.org\/10.5281\/zenodo.12669638 10.5281\/zenodo.12669638","DOI":"10.5281\/zenodo.12669638"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:14:21Z","timestamp":1770196461000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689719"],"URL":"https:\/\/doi.org\/10.1145\/3689719","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}