Generative Type-Aware Mutation for Testing SMT Solvers
summary
Generative Type-Aware Mutation implements expression mutation using SMT-LIB operator signatures to produce grammatically correct but larger mutants, realized in the tool TypeFuzz built on yinyang. The method guarantees an unbounded mutation space by allowing new operators whose argument types exist in the seed, and it finds concrete failures: over 70 bugs reported across Z3 and CVC4, 48 confirmed and 35 fixed, including 9 soundness bugs in CVC4 (three latent ≥2 years).
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:17SMT Problem
- 1:14SMT-LIB language
- 2:05Bug in SMT Solver
- 3:31Generative Type-Aware Mutation
- 5:11Empirical Evaluation
- 7:39Bug Findings in Z3's new core
- 7:54Coverage Evaluation
- 8:45Bugs Affecting Historic Releases
- 9:18Z3 Soundness Bug #5429
- 10:30CVC4 Soundness Bug #6075 58
- 11:15CVC4 Crash Bug #6228
- 11:55Future Work
- 12:12yinyang -a fuzzing framework for SMT Solvers
related talks
13mOn the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
14mFuzzing C++ Compilers via Type-Driven Mutation
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
22mKill All Mutants! (Introduction to Mutation Testing)
35mKill All Mutants! (Intro to Mutation Testing)
15mTowards Proof Stability in SMT-based Program Verification
29mKill All Mutants! (Intro to Mutation Testing)
45mMutation Testing