Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
summary
ET is a grammar-based enumerator that compiles eight SMT theory grammars into algebraic datatypes and drives the FEAT enumerator to produce smallest-to-largest formulas for differential testing. Running on 61 Z3 and CVC4/cvc5 releases it checks 8 million formulas and issues 488 million solver calls, finds 102 bugs (76 confirmed, 32 fixed), and exposes performance regressions: Z3 slows on short timeouts since z3-4.8.11 and early cvc5 releases regress on long timeouts. Results support using ET for continuous integration.
AI-written summary · about
chapters (13)
- 0:00ET and SMT solver validation
- 1:51Limitations in SMT testing
- 3:36Small bug triggers matter
- 5:44Grammar-based enumeration
- 7:15Validation results and bugs
- 8:39Performance bugs detection
- 9:44Z3 and CVC5 correctness
- 11:30Performance evolution
- 13:21Have we tested enough?
- 14:46Can testing prove absence?
- 15:29Q&A: Property-based testing
- 18:03Q&A: Enumerative testing impact
- 19:48Q&A: Future work
related talks
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
28mEtna: An Evaluation Platform for Property-Based Testing
20mAutomatic Repair of Regular Expressions
16mSoftware Model Checking via Summary-Guided Search
12mGenerative Type-Aware Mutation for Testing SMT Solvers
15mGrammar-Based Testing for Little Languages: An Experience Report with Student Compilers
19mCovering All the Bases: Type-Based Verification of Test Input Generators