12 citations · 16 across the 3 of their papers we have counts for
6 papers
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…
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…
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…
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
Andrew Reynolds, Morgan Deters, Viktor Kuncak +2
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negate…