“Verifying SQL queries using theories of tables and relations” by Mudathir Mahgoub Yahia Mohamed, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '24), (Nikolaj Bjørner, Marijn Heule, and Andrei Voronkov, eds.), May 2024, pp. 445-463. Port Louis, Mauritius.
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.
BibTeX entry:
@inproceedings{MRT+24,
author = {Mudathir Mahgoub Yahia Mohamed and Andrew Reynolds and Cesare
Tinelli and Clark Barrett},
editor = {Nikolaj Bj{\o}rner and Marijn Heule and Andrei Voronkov},
title = {Verifying {SQL} queries using theories of tables and relations},
booktitle = {Proceedings of 25th Conference on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR '24)},
series = {EPiC Series in Computing},
volume = {100},
pages = {445--463},
publisher = {EasyChair},
month = may,
year = {2024},
doi = {10.29007/rlt7},
note = {Port Louis, Mauritius},
url = {http://theory.stanford.edu/~barrett/pubs/MRT+24.pdf}
}
(This webpage was created with bibtex2web.)