VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity(…)
summary
VeriEQL encodes SQL semantics over symbolic tuples using an SMT encoding with integers and uninterpreted functions and checks bounded equivalence by symbolically executing both queries under schema integrity (PK/FK/NOT NULL) and list semantics including ORDER BY. Evaluation on >20,000 benchmarks shows it proves or disproves equivalence for ~75% and outperforms prior tools by >10×; generated counterexamples are typically tiny (2–3 rows) and expose real bugs in MySQL and Apache Calcite and 3,500+ incorrect LeetCode submissions.
AI-written summary · about
chapters (9)
- 0:00VeriEQL introduction
- 1:25Why SQL equivalence matters
- 3:53Challenges in SQL verification
- 6:30Formalizing SQL semantics
- 9:00VeriEQL symbolic execution
- 14:01Benchmarking VeriEQL
- 16:54Real-world impact
- 17:15Future directions
- 18:20Q&A
related talks
14mDetecting Logic Bugs in Database Engines via Equivalent Expression Transformation
20mGraphiti: Bridging Graph and Relational Database Queries
18mTranslating canonical SQL to imperative code in Coq
17mBetter Together: Unifying Datalog and Equality Saturation
14mChecking Observational Correctness of Database Systems
18mValScope: Value-Semantics-Aware Metamorphic Testing for Detecting Logical Bugs in DBMSs
15mSpeeding up Symbolic Reasoning for Relational Queries
35mLogical Interfaces to Data, Beyond Views