Verifying SQL Queries using Theories of Tables and Relations

TL;DR

This paper introduces new SMT theories to accurately model and verify SQL queries involving joins, projections, selections, nulls, and different semantics, enhancing automated reasoning capabilities.

Contribution

It extends SMT theories to handle SQL-specific features like bags, relations, null values, and query semantics, with implementations in cvc5 for improved query verification.

Findings

Successfully modeled SQL queries with various features in SMT theories.

Implemented solvers in cvc5 that verify SQL query equivalences.

Evaluated on benchmarks showing effectiveness of the approach.

Abstract

We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operations. We support reasoning about SQL queries with either bag or set semantics for database tables. We provide the former via an extension of a theory of finite bags and the latter via an extension of the theory of finite relations. Furthermore, we add the ability to reason about tables with null values by introducing a theory of nullable sorts based on an extension of the theory of algebraic datatypes. We implemented solvers for these theories in the SMT solver cvc5 and evaluated them on a set of benchmarks derived from public sets of SQL equivalence problems.