Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
summary
Aries validates SMT rewriters by combining mimetic mutation that reshapes seed formulas to match rewrite left‑hand sides with generative equality saturation (an e‑graph engine modified to allow rewrites that introduce variables) to exhaust the rewrite space, extract many semantically equivalent mutants, and cross‑check Z3 and cvc5 on SMT‑LIB benchmarks. The tool uses rules from cvc5 and synthesized rules from ruler, applies a structural sampling strategy, and finds 27 new issues of which 22 are confirmed or fixed, covering correctness, crashes, completeness, and performance.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 2:32SMT rewriters' role
- 5:11Testing SMT rewriters
- 5:53Two-phase rewriter validation
- 8:49Deductive rewriting with equality saturation
- 11:21Implementation and evaluation
- 13:35Summary and Q&A
related talks
29mSemantic Transformation Framework for Rewriting Rules
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
12mGenerative Type-Aware Mutation for Testing SMT Solvers
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
15mTowards Proof Stability in SMT-based Program Verification
30mAnalyzing Programs with SMT Solvers
14mRewrite Rule Inference Using Equality Saturation
13mOn the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers