23 citations · 68 across the 21 of their papers we have counts for
26 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…
The SemGuS Toolkit
Keith J. C. Johnson, Andrew Reynolds, Thomas Reps +1
Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS fo…
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…
The SyGuS Language Standard Version 2.1
Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman +2
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Syntax-guided synthesis (SyGuS) i…
Partitioning Strategies for Distributed SMT Solving
Amalee Wilson, Andres Noetzli, Andrew Reynolds +3
For many users of Satisfiability Modulo Theories (SMT) solvers, the solver's performance is the main bottleneck in their application. One promising approach for improving performan…
Reasoning About Vectors using an SMT Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds +7
Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such progra…
Satisfiability and Synthesis Modulo Oracles
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification)…
Fair and Adventurous Enumeration of Quantifier Instantiations
Mikoláš Janota, Haniel Barbosa, Pascal Fontaine +1
SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier ins…
lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann +3
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Politeness and Stable Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by…
CVC4SY for SyGuS-COMP 2019
Andrew Reynolds, Haniel Barbosa, Andres Nötzli +2
CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term enumeration and, for restricted fragments, quantifier elimination. The enumerative strategies are based on…
Towards Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds +3
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors…
CVC4 at the SMT Competition 2018
Clark Barrett, Haniel Barbosa, Martin Brain +8
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For f…
On Solving Quantified Bit-Vectors using Invertibility Conditions
Aina Niemetz, Mathias Preiner, Andrew Reynolds +2
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We deri…
SyGuS Techniques in the Core of an SMT Solver
Andrew Reynolds, Cesare Tinelli
We give an overview of recent techniques for implementing syntax-guided synthesis (SyGuS) algorithms in the core of Satisfiability Modulo Theories (SMT) solvers. We define several…
Constraint Solving for Finite Model Finding in SMT Solvers
Andrew Reynolds, Cesare Tinelli, Clark Barrett
SMT solvers have been used successfully as reasoning engines for automated verification and other applications based on automated reasoning. Current techniques for dealing with qua…
Reasoning with Finite Sets and Cardinality Constraints in SMT
Kshitij Bansal, Clark Barrett, Andrew Reynolds +1
We consider the problem of deciding the satisfiability of quantifier-free formulas in the theory of finite sets with cardinality constraints. Sets are a common high-level data stru…
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic
Andrew Reynolds, Radu Iosif, Cristina Serban
Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investi…
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Burak Ekici, Guy Katz, Chantal Keller +3
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic…
A Decision Procedure for Separation Logic in SMT
Andrew Reynolds, Radu Iosif, Tim King
This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over…
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic
Andrew Reynolds, Tim King, Viktor Kuncak
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, impl…
On Deciding Local Theory Extensions via E-matching
Kshitij Bansal, Andrew Reynolds, Tim King +2
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automat…