Verifying SQL Queries using Theories of Tables and Relations

Mudathir Mohamed; Andrew Reynolds; Cesare Tinelli; Clark Barrett

doi:10.48550/arxiv.2405.03057

Back

Verifying SQL Queries using Theories of Tables and Relations

Preprint

Open access

Verifying SQL Queries using Theories of Tables and Relations

Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli and Clark Barrett

ArXiv.org

Cornell University

05/05/2024

DOI: 10.48550/arxiv.2405.03057

Files and links (1)

url

https://doi.org/10.48550/arxiv.2405.03057View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

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.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Verifying SQL Queries using Theories of Tables and Relations
Creators: Mudathir Mohamed - University of Iowa
Andrew Reynolds - University of Iowa
Cesare Tinelli - University of Iowa
Clark Barrett - Stanford University
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2405.03057
ISSN: 2331-8422
Publisher: Cornell University; Ithaca, New York
Language: English
Date posted: 05/05/2024
Academic Unit: Computer Science
Record Identifier: 9984622897502771

Metrics

72 Record Views