Towards Proof Stability in SMT-based Program Verification
summary
Paper and prototype work presents a mutation-driven detector Mariposa mutation-based detector and an SMT-level pruning algorithm that use Z3 proof-of-unsat and Z3 instantiation traces to localize instability to individual quantifiers. A measurement over five Dafny/F query sets and tens of thousands of queries finds >96% of query context is irrelevant and pruning mitigates 70–78% of instability. On the Varys benchmark of 70 unstable queries, 62 stabilize with a single-quantifier edit*, four are unfixable by that edit, four fail analysis.
AI-written summary · about
chapters (8)
- 0:00Proof stability in SMT verification
- 1:25Automation versus stability trade-off
- 2:28Detecting unstable SMT queries with Mariposa
- 4:36Irrelevant context in SMT queries
- 5:59Debugging unstable quantifiers
- 10:41Quantifier debugging results
- 11:46Repairing unstable proofs
- 13:34Key takeaways on proof stability
related talks
13mOn the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
12mGenerative Type-Aware Mutation for Testing SMT Solvers
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
13mProgram Analysis via Efficient Symbolic Abstraction
27mTaming Unsoundness with Gradual Abstract Interpretation