6 papers
Automated Reasoning with Nested Datatypes
Tomer Hakak, Yoni Zohar, Andrew Reynolds +2
We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging.…
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…
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan +5
Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof ass…
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz +4
In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncomm…
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…
Generalized Optimization Modulo Theories
Nestan Tsiskaridze, Clark Barrett, Cesare Tinelli
Optimization Modulo Theories (OMT) has emerged as an important extension of the highly successful Satisfiability Modulo Theories (SMT) paradigm. The OMT problem requires solving an…