Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
summary
Canary runs differential testing on Z3 and CVC5 and systematically partitions solutions with three bounded mutation strategies — numerical domains, boolean cubes, and quantifier injection — to force solvers into different semantic subspaces. The implementation generates constrained subformulas, finds 123 unique crashes or disagreements of which 108 are confirmed and 107 fixed, with ~35% being soundness/invalid-model issues, raises line/branch coverage (≈0.7 percentage points in one integration) and uncovers bugs across bitvectors, arrays, and nonlinear arithmetic.
AI-written summary · about
chapters (14)
- 0:00SMT solver testing challenges
- 2:12Critical solver bugs and impact
- 3:19Limitations of testing methods
- 4:44Motivating example: solver differences
- 6:28Subspace diversification technique
- 7:11Partitioning with numerical domains
- 7:56Boolean cubes for exploration
- 8:41Quantifier partitioning for logic
- 9:44Canary workflow and testing
- 10:29Evaluating Canary's bug finding
- 11:52Code coverage with Canary
- 13:42Bug discovery rates impact
- 15:12Conclusion and future work
- 16:37Q&A
related talks
21mValidating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
18mSMT2Test: From SMT Formulas to Effective Test Cases
01h 10mA Roadmap for the Next Phase of SAT Research
16mSoftware Model Checking via Summary-Guided Search
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
12mGenerative Type-Aware Mutation for Testing SMT Solvers
34mSymbolic Execution for Randomized Programs
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...