Hatching Theory Instantiations with Yardbird
summary
Yardbird is a CEGAR framework that uses egg’s equality saturation engine to hatch array theory instantiations: axioms become rewrite rules, e-classes that should merge mark theory conflicts, and refinements are chosen by custom cost functions. The prototype extracts instantiations from Z3 models and applies property-directed cost function or size heuristics. Evaluated on 193 SV-COMP array benchmarks, it beats Z3 on 26% for runtime and reduces quantifier instantiations on 49%; results show clear gains but no one-size-fits-all heuristic.
AI-written summary · about
chapters (9)
- 0:00Hatching Theory intro
- 1:04Bounded model checking with arrays
- 2:26Technique overview and Rust translation
- 3:49BMC with full array theory
- 4:50Abstraction and refinement in BMC
- 6:15Cost functions for term selection
- 7:41Cost functions comparison in Yardbird
- 9:29Conclusions and future work
- 11:35Q&A
related talks
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
30megg: Fast and Extensible Equality Saturation
17mBetter Together: Unifying Datalog and Equality Saturation
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
19mPanel: Compilation Frameworks