VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints

VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints

April 2024 | YANG HE, Simon Fraser University, Canada; PINHAN ZHAO, University of Michigan, USA; XINYU WANG, University of Michigan, USA; YUEPENG WANG, Simon Fraser University, Canada
VeriEQL is a novel approach for bounded equivalence verification of complex SQL queries with integrity constraints. It is the first SMT-based method capable of proving and disproving equivalence for such queries. VeriEQL uses a new logical encoding that models query semantics over symbolic tuples using integers with uninterpreted functions. This encoding is simple yet highly practical, as demonstrated by its performance on over 20,000 benchmarks, where it outperforms all state-of-the-art techniques by more than one order of magnitude. VeriEQL can also generate counterexamples, which are useful for finding bugs in systems like MySQL and Apache Calcite. The paper formulates the problem of bounded SQL equivalence verification modulo integrity constraints, formalizes the semantics of a practical fragment of SQL queries, proposes a novel SMT encoding, proves its correctness, and implements VeriEQL. The evaluation shows that VeriEQL can solve 77% of the benchmarks, while state-of-the-art bounded verifiers can solve less than 2%.VeriEQL is a novel approach for bounded equivalence verification of complex SQL queries with integrity constraints. It is the first SMT-based method capable of proving and disproving equivalence for such queries. VeriEQL uses a new logical encoding that models query semantics over symbolic tuples using integers with uninterpreted functions. This encoding is simple yet highly practical, as demonstrated by its performance on over 20,000 benchmarks, where it outperforms all state-of-the-art techniques by more than one order of magnitude. VeriEQL can also generate counterexamples, which are useful for finding bugs in systems like MySQL and Apache Calcite. The paper formulates the problem of bounded SQL equivalence verification modulo integrity constraints, formalizes the semantics of a practical fragment of SQL queries, proposes a novel SMT encoding, proves its correctness, and implements VeriEQL. The evaluation shows that VeriEQL can solve 77% of the benchmarks, while state-of-the-art bounded verifiers can solve less than 2%.
Reach us at info@study.space
[slides and audio] VeriEQL%3A Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints