CVC4. - Clark W. Barrett; Christopher L. Conway; Morgan Deters; Liana Hadarean; Dejan Jovanovic; Tim King 001; Andrew Reynolds 001; Cesare Tinelli (CAV, 2011)

LFSC for SMT Proofs: Work in Progress. - Aaron Stump; Andrew Reynolds 001; Cesare Tinelli; Austin Laugesen; Harley Eades III; Corey Oliver; Ruoyu Zhang (PxTP, 2012)

Quantifier Instantiation Techniques for Finite Model Finding in SMT. - Andrew Reynolds 001; Cesare Tinelli; Amit Goel; Sava Krstic; Morgan Deters; Clark W. Barrett (CADE, 2013)

Finite Model Finding in SMT. - Andrew Reynolds 001; Cesare Tinelli; Amit Goel; Sava Krstic (CAV, 2013)

SMT proof checking using a logical framework. - Aaron Stump; Duckki Oe; Andrew Reynolds 001; Liana Hadarean; Cesare Tinelli (Formal Methods Syst. Des., 2013)

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. - Tianyi Liang; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett; Morgan Deters (CAV, 2014)

A tour of CVC4: How it works, and how to use it. - Morgan Deters; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2014)

Finding conflicting instances of quantified formulas in SMT. - Andrew Reynolds 001; Cesare Tinelli; Leonardo Mendonça de Moura (FMCAD, 2014)

Approaches for Synthesis Conjectures in an SMT Solver. - Andrew Reynolds 001 (CoRR, 2014)

Deciding Local Theory Extensions via E-matching. - Kshitij Bansal; Andrew Reynolds 001; Tim King 001; Clark W. Barrett; Thomas Wies (CAV (2), 2015)

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. - Andrew Reynolds 001; Morgan Deters; Viktor Kuncak; Cesare Tinelli; Clark W. Barrett (CAV (2), 2015)

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. - Tianyi Liang; Nestan Tsiskaridze; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (FroCos, 2015)

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. - Liana Hadarean; Clark W. Barrett; Andrew Reynolds 001; Cesare Tinelli; Morgan Deters (LPAR, 2015)

Induction for SMT Solvers. - Andrew Reynolds 001; Viktor Kuncak (VMCAI, 2015)

An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. - Andrew Reynolds 001; Tim King 001; Viktor Kuncak (CoRR, 2015)

On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. - Andrew Reynolds 001; Morgan Deters; Viktor Kuncak; Clark W. Barrett; Cesare Tinelli (CoRR, 2015)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Cristina Serban; Tim King 001 (ATVA, 2016)

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. - Kshitij Bansal; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (IJCAR, 2016)

Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. - Andrew Reynolds 001 (Vampire@IJCAR, 2016)

Model Finding for Recursive Functions in SMT. - Andrew Reynolds 001; Jasmin Christian Blanchette; Simon Cruanes; Cesare Tinelli (IJCAR, 2016)

Lazy proofs for DPLL(T)-based SMT solvers. - Guy Katz; Clark W. Barrett; Cesare Tinelli; Andrew Reynolds 001; Liana Hadarean (FMCAD, 2016)

Efficient solving of string constraints for security analysis. - Clark W. Barrett; Cesare Tinelli; Morgan Deters; Tianyi Liang; Andrew Reynolds 001; Nestan Tsiskaridze (HotSoS, 2016)

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). - Burak Ekici; Guy Katz; Chantal Keller; Alain Mebsout; Andrew J. Reynolds; Cesare Tinelli (HaTT@IJCAR, 2016)

A Decision Procedure for Separation Logic in SMT. - Andrew Reynolds 001; Radu Iosif; Tim King 001 (CoRR, 2016)

Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic. - Andrew Reynolds 001; Radu Iosif; Cristina Serban (CoRR, 2016)

An efficient SMT solver for string constraints. - Tianyi Liang; Andrew Reynolds 001; Nestan Tsiskaridze; Cesare Tinelli; Clark W. Barrett; Morgan Deters (Formal Methods Syst. Des., 2016)

Relational Constraint Solving in SMT. - Baoluo Meng; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (CADE, 2017)

Challenges for Fast Synthesis Procedures in SMT. - Andrew Reynolds 001 (ARCADE@CADE, 2017)

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. - Burak Ekici; Alain Mebsout; Cesare Tinelli; Chantal Keller; Guy Katz; Andrew Reynolds 001; Clark W. Barrett (CAV (2), 2017)

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. - Andrew Reynolds 001; Maverick Woo; Clark W. Barrett; David Brumley; Tianyi Liang; Cesare Tinelli (CAV (2), 2017)

Designing Theory Solvers with Extensions. - Andrew Reynolds 001; Cesare Tinelli; Dejan Jovanovic; Clark W. Barrett (FroCoS, 2017)

Quantifier Instantiation Beyond E-Matching. - Andrew Reynolds 001 (SMT, 2017)

Congruence Closure with Free Variables. - Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (TACAS (2), 2017)

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. - Andrew Reynolds 001; Radu Iosif; Cristina Serban (VMCAI, 2017)

SyGuS Techniques in the Core of an SMT Solver. - Andrew Reynolds 001; Cesare Tinelli (SYNT@CAV, 2017)

Solving quantified linear arithmetic by counterexample-guided instantiation. - Andrew Reynolds 001; Tim King 001; Viktor Kuncak (Formal Methods Syst. Des., 2017)

A Decision Procedure for (Co)datatypes in SMT Solvers. - Andrew Reynolds 001; Jasmin Christian Blanchette (J. Autom. Reason., 2017)

Constraint solving for finite model finding in SMT solvers. - Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (Theory Pract. Log. Program., 2017)

Datatypes with Shared Selectors. - Andrew Reynolds 001; Arjun Viswanathan 001; Haniel Barbosa; Cesare Tinelli; Clark W. Barrett (IJCAR, 2018)

Solving Quantified Bit-Vectors Using Invertibility Conditions. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CAV (2), 2018)

The FMCAD 2018 Graduate Student Forum. - Dejan Jovanovic; Andrew Reynolds 001 (FMCAD, 2018)

Revisiting Enumerative Instantiation. - Andrew Reynolds 001; Haniel Barbosa; Pascal Fontaine (TACAS (2), 2018)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

Reasoning with Finite Sets and Cardinality Constraints in SMT. - Kshitij Bansal; Clark W. Barrett; Andrew Reynolds 001; Cesare Tinelli (Log. Methods Comput. Sci., 2018)

Extending SMT Solvers to Higher-Order Logic. - Haniel Barbosa; Andrew Reynolds 001; Daniel El Ouraoui; Cesare Tinelli; Clark W. Barrett (CADE, 2019)

Towards Bit-Width-Independent Proofs in SMT Solvers. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (CADE, 2019)

Invertibility Conditions for Floating-Point Formulas. - Martin Brain; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

High-Level Abstractions for Simplifying Extended String Constraints in SMT. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

Extending enumerative function synthesis via SMT-driven classification. - Haniel Barbosa; Andrew Reynolds 001; Daniel Larraz; Cesare Tinelli (FMCAD, 2019)

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Clark W. Barrett; Cesare Tinelli (SAT, 2019)

SL-COMP: Competition of Solvers for Separation Logic. - Mihaela Sighireanu; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds 001; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll 001; Florian Zuleger; Wei-Ngan Chin; et al. (TACAS (3), 2019)

CVC4SY for SyGuS-COMP 2019. - Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (CoRR, 2019)

Refutation-based synthesis in SMT. - Andrew Reynolds 001; Viktor Kuncak; Cesare Tinelli; Clark W. Barrett; Morgan Deters (Formal Methods Syst. Des., 2019)

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. - Andrew Reynolds 001; Haniel Barbosa; Daniel Larraz; Cesare Tinelli (IJCAR (1), 2020)

A Decision Procedure for String to Code Point Conversion. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (IJCAR (1), 2020)

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. - M. Fareed Arif; Daniel Larraz; Mitziu Echeverria; Andrew Reynolds 001; Omar Chowdhury; Cesare Tinelli (FMCAD, 2020)

Reductions for Strings and Regular Expressions Revisited. - Andrew Reynolds 001; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (FMCAD, 2020)

Politeness and Stable Infiniteness: Stronger Together. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CADE, 2021)

Fair and Adventurous Enumeration of Quantifier Instantiations. - Mikolás Janota; Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (FMCAD, 2021)

Characteristic Subsets of SMT-LIB Benchmarks. - Jan Jakubuv; Mikolás Janota; Andrew Reynolds 001 (SMT, 2021)

Syntax-Guided Quantifier Instantiation. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (TACAS (2), 2021)

lazybvtoint at the SMT Competition 2020. - Yoni Zohar; Ahmed Irfan; Makai Mann; Andres Nötzli; Andrew Reynolds 001; Clark W. Barrett (CoRR, 2021)

On solving quantified bit-vector constraints using invertibility conditions. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (Formal Methods Syst. Des., 2021)

Towards Satisfiability Modulo Parametric Bit-vectors. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2021)

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (Zenodo, 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). - Gereon Kremer; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Even Faster Conflicts and Lazier Reductions for String Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Clark W. Barrett; Cesare Tinelli (CAV (2), 2022)

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. - Andres Nötzli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2022)

cvc5: A Versatile and Industrial-Strength SMT Solver. - Haniel Barbosa; Clark W. Barrett; Martin Brain; Gereon Kremer; Hanna Lachnitt; Makai Mann; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; et al. (TACAS (1), 2022)

Satisfiability and Synthesis Modulo Oracles. - Elizabeth Polgreen; Andrew Reynolds 001; Sanjit A. Seshia (VMCAI, 2022)

Bit-Precise Reasoning via Int-Blasting. - Yoni Zohar; Ahmed Irfan; Makai Mann; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (VMCAI, 2022)

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. - Abdalrhman Mohamed; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2023)

Partitioning Strategies for Distributed SMT Solving. - Amalee Wilson; Andres Nötzli; Andrew Reynolds 001; Byron Cook; Cesare Tinelli; Clark W. Barrett (FMCAD, 2023)

An Interactive SMT Tactic in Coq using Abductive Reasoning. - Haniel Barbosa; Chantal Keller; Andrew Reynolds 001; Arjun Viswanathan 001; Cesare Tinelli; Clark W. Barrett (LPAR, 2023)

Selecting Quantifiers for Instantiation in SMT. - Jan Jakubuv; Mikolás Janota; Bartosz Piotrowski; Jelle Piepenbrock; Andrew Reynolds 001 (SMT, 2023)

Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (SMT, 2023)

The SyGuS Language Standard Version 2.1. - Saswat Padhi; Elizabeth Polgreen; Mukund Raghothaman; Andrew Reynolds 001; Abhishek Udupa (CoRR, 2023)

Synthesising Programs with Non-trivial Constants. - Alessandro Abate; Haniel Barbosa; Clark W. Barrett; Cristina David; Pascal Kesseli; Daniel Kroening; Elizabeth Polgreen; Andrew Reynolds 001; Cesare Tinelli (J. Autom. Reason., 2023)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (Zenodo, 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

Combining Stable Infiniteness and (Strong) Politeness. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

The SemGuS Toolkit. - Keith J. C. Johnson; Andrew Reynolds 001; Thomas W. Reps; Loris D'Antoni (CAV (3), 2024)

Satisfiability Modulo Theories: A Beginner's Tutorial. - Clark W. Barrett; Cesare Tinelli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar (FM (2), 2024)

SMT-D: New Strategies for Portfolio-Based SMT Solving. - Clark W. Barrett; Pei-Wei Chen; Byron Cook; Bruno Dutertre; Robert B. Jones; Nham Le; Andrew Reynolds 001; Kunal Sheth; Christopher Stephens; Michael W. Whalen (FMCAD, 2024)

Verifying SQL queries using theories of tables and relations. - Mudathir Mohamed; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (LPAR, 2024)

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. - Hanna Lachnitt; Mathias Fleury; Leni Aniva; Andrew Reynolds 001; Haniel Barbosa; Andres Nötzli; Clark W. Barrett; Cesare Tinelli (TACAS (1), 2024)

Using Normalization to Improve SMT Solver Stability. - Daneshvar Amrollahi; Mathias Preiner; Aina Niemetz; Andrew Reynolds 001; Moses Charikar; Cesare Tinelli; Clark W. Barrett (CoRR, 2024)

cvc5 for SMT-COMP 2024. - Leni Aniva; Haniel Barbosa; Clark W. Barrett; Hanna Lachnitt; Daniel Larraz; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Hans-Jörg Schurr; et al. (Zenodo, 2024)

cvc5-cloud. - Amalee Wilson; Andres Nötzli; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett (Zenodo, 2024)

lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (CAV (3), 2025)

Bit-Precise Reasoning with Parametric Bit-Vectors. - Zvika Berger; Yoni Zohar; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (SAT, 2025)

Augmenting Model-Based Instantiation with Fast Enumeration. - Lydia Kondylidou; Andrew Reynolds 001; Jasmin Blanchette (TACAS (1), 2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Harun Khan; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (CoRR, 2025)

Solving Set Constraints with Comprehensions and Bounded Quantifiers. - Mudathir Mohamed; Nick Feng; Andrew Reynolds 001; Cesare Tinelli; Clark W. Barrett; Marsha Chechik (CoRR, 2025)