Verifying SQL Queries using Theories of Tables and Relations
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909210888896512 |
|---|---|
| author | Mohamed, Mudathir Reynolds, Andrew Tinelli, Cesare Barrett, Clark |
| author_facet | Mohamed, Mudathir Reynolds, Andrew Tinelli, Cesare Barrett, Clark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_03057 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Verifying SQL Queries using Theories of Tables and Relations Mohamed, Mudathir Reynolds, Andrew Tinelli, Cesare Barrett, Clark Logic in Computer Science 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. |
| title | Verifying SQL Queries using Theories of Tables and Relations |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2405.03057 |