On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
summary
Proposes type-aware operator mutation: randomly replace operators with others of the same SMT-LIB type, chain mutations, and cross-check Z3 vs CVC4 to spot divergences. Implements it in the fuzzer OpFuzz and runs a year-long campaign on 300k seeds, reporting 1,092 bugs (819 unique confirmed, 685 fixed), including 184 soundness and 102 invalid-model bugs; root causes include unsound rewrite rules (bvxnor), missed cases in str.indexof, and unsafe simplifications.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:18SMT Problem
- 1:33SMT-LIB language
- 1:55SMT Solver Bug
- 2:28Related Work
- 4:41Type-aware operator mutation chain
- 6:15Bug Findings
- 7:20Comparison to Previous Approaches
- 7:45Z3 Soundness Bug #2832
- 9:17CVC4 Soundness Bug #3497
- 10:50Discussion
- 12:30Summary SMT Solver
- 13:12Yin-Yang Umbrella Release
related talks
12mGenerative Type-Aware Mutation for Testing SMT Solvers
14mFuzzing C++ Compilers via Type-Driven Mutation
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
15mTowards Proof Stability in SMT-based Program Verification
13mProgram Analysis via Efficient Symbolic Abstraction
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
53mLocknote: How Badly Do We Want Correct Compilers?
14mFinding Compiler Bugs through Cross-Language Code Generator and Differential Testing