Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025
Solving Set Constraints with Comprehensions and Bounded Quantifiers
Mudathir Mohamed, Nick Feng, Andrew Reynolds +3
Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Differe…
cs.LO2024
Verifying SQL Queries using Theories of Tables and Relations
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli +1
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 operatio…