Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries

Download PDF

Abstract

Equivalence checking for SQL queries has many real-world applications but typically requires supporting an expressive SQL language in order to be practical. We develop VeriEQL, a system that can prove and disprove equivalence of complex SQL queries. Specifically, given two SQL queries under a database schema, VeriEQL can verify whether these two queries always produce identical results on all possible input databases up to a bounded size that conform to the schema. This paper demonstrates VeriEQL in three scenarios, including validating the correctness of query optimizations, grading SQL queries on online coding platforms, and finding implementation bugs in database management systems.