KestRel: Relational Verification Using E-Graphs for Program Alignment
summary
KestRel builds an intermediate product program via an algebra of alignments, represents the rewrite search in e-graphs and equality saturation, and extracts semantically useful alignments with data-driven MCMC extraction over execution traces. Implementation hands aligned programs to Seahor, Daphne, and Dicon for verification. On literature benchmarks KestRel aligns and verifies nearly all cases within a minute; one benchmark needs novel loop-guard synthesis, and in an ADT suite two fail (one synthesis, one backing invariant inference), artifacts and code are available.
AI-written summary · about
chapters (10)
- 0:00Program alignment in verification
- 1:04Relational verification challenges
- 2:50Product programs and alignment
- 4:13KestRel for automatic alignment
- 5:58Alignment algebra and rules
- 7:21Egraphs for alignment space
- 8:45Datadriven optimal alignment
- 10:50Evaluation results and benchmarks
- 12:35Summary and future directions
- 13:40Q&A
related talks
15mHEC: Equivalence Verification Checking for Code Transformation via Equality...
16mMulti-stage Relational Programming
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
17mBetter Together: Unifying Datalog and Equality Saturation
20mEquality Saturation and Joins
19mAutomated Verification of Fundamental Algebraic Laws
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
01h 03mMatching Logic: Foundation of the K Framework