SMT2Test: From SMT Formulas to Effective Test Cases

on YouTube ↗18m

" summary

SMT2Test transforms SMT formulas into executable programs (Dafny and C via an intermediate representation) and encodes satisfiability as a reachability assertion so SMT solver responses serve as test oracles. The implementation uses SMT competition benchmarks and SMT-fuzzer seeds (Z3/CVC5 style solvers) and reports 14 previously unknown defects, with 6 fixed after reporting. The tool uncovers both deep soundness bugs and rewriting errors, validating verifiers like Dafny and CPAchecker.

AI-written summary · about

" chapters (6)

1. 0:00Test case generation with SMT
2. 3:09SMT to test case challenges
3. 7:24SMT to program conversion
4. 9:51Evaluating verifiers and bugs
5. 13:27Summary and future of SMT2Test
6. 15:13Q&A on false positives

" related talks

• 17mDafny Test GenerationAleksandr Fedchin, Jeffrey S. Foster, Aaron Tomb, Zvonimir Rakamaric · Dafny 2024
• 21mBounded-Exhaustive Subspace Diversification for SMT Solver TestingPeisen Yao, Junda Zheng · SAS 2025
• 46mIntroduction to Formal Verification with Symbiotic EDA Open Source ToolsMatt Venn, Clifford Wolf · Week of Open Source Hardware 2019
• 16mSoftware Model Checking via Summary-Guided SearchRuijie Fang, Zachary Kincaid, Thomas Reps · OOPSLA 2025
• 20mBeyond Fuzzing Symbolic Testing in PracticeDaniel Karmacoma · Solidity Summit 2023
• 16mRandomised Testing of the Dafny CompilerAlastair F. Donaldson, Jean-Baptiste Tristan, Dilan Sheth, Alex Usher · Dafny 2024
• 23mHUSTEF 2014 - Stephan SchulzStephan Schulz · HUSTEF 2014
• 30mGenerating Conforming Programs With XsmithSorawee Porncharoenwase, Pierce Darragh, Eric Eide, William Gallard Hatch, Guy Watson · GPCE 2023