Andrew Reynolds

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 81

Top Topics

Constraint Solving

Modulo Theories

Automated Reasoning

Top Venues

Publications

Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Verifying SQL Queries using Theories of Tables and Relations. CoRR (2024)
Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni
The SemGuS Toolkit. CoRR (2024)
Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni
The SemGuS Toolkit. CAV (3) (2024)
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Verifying SQL queries using theories of tables and relations. LPAR (2024)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) (2024)
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67 (3) (2023)
Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, Abhishek Udupa
The SyGuS Language Standard Version 2.1. CoRR (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. CoRR (2023)
Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD (2023)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67 (4) (2023)
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
Synthesising Programs with Non-trivial Constants. J. Autom. Reason. 67 (2) (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. FMCAD (2023)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT (2023)
Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
Selecting Quantifiers for Instantiation in SMT. SMT (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Bit-Precise Reasoning via Int-Blasting. VMCAI (2022)
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR (2022)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) (2022)
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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR (2022)
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD (2022)
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
Satisfiability and Synthesis Modulo Oracles. VMCAI (2022)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR (2021)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CADE (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65 (7) (2021)
Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia
Satisfiability and Synthesis Modulo Oracles. CoRR (2021)
Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett
lazybvtoint at the SMT Competition 2020. CoRR (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Quantifier Instantiation. TACAS (2) (2021)
Jan Jakubuv, Mikolás Janota, Andrew Reynolds
Characteristic Subsets of SMT-LIB Benchmarks. SMT (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CoRR (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57 (1) (2021)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Reductions for Strings and Regular Expressions Revisited. FMCAD (2020)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
A Decision Procedure for String to Code Point Conversion. IJCAR (1) (2020)
M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. FMCAD (2020)
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) (2020)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE (2019)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
CVC4SY for SyGuS-COMP 2019. CoRR (2019)
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
Extending SMT Solvers to Higher-Order Logic. CADE (2019)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT (2019)
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55 (2) (2019)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) (2019)
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
Extending enumerative function synthesis via SMT-driven classification. FMCAD (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR (2019)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Invertibility Conditions for Floating-Point Formulas. CAV (2) (2019)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) (2019)
Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu
SL-COMP: Competition of Solvers for Separation Logic. TACAS (3) (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR (2018)
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. 14 (4) (2018)
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
Revisiting Enumerative Instantiation. TACAS (2) (2018)
Dejan Jovanovic, Andrew Reynolds
The FMCAD 2018 Graduate Student Forum. FMCAD (2018)
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
Datatypes with Shared Selectors. IJCAR (2018)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) (2018)
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
CVC4 at the SMT Competition 2018. CoRR (2018)
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) (2017)
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR (2017)
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Congruence Closure with Free Variables. TACAS (2) (2017)
Andrew Reynolds, Cesare Tinelli
SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV (2017)
Andrew Reynolds, Radu Iosif, Cristina Serban
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. VMCAI (2017)
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17 (4) (2017)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58 (3) (2017)
Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) (2017)
Andrew Reynolds, Tim King, Viktor Kuncak
Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51 (3) (2017)
Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Relational Constraint Solving in SMT. CADE (2017)
Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett
Designing Theory Solvers with Extensions. FroCoS (2017)
Andrew Reynolds
Challenges for Fast Synthesis Procedures in SMT. ARCADE@CADE (2017)
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR (2017)
Andrew Reynolds
Quantifier Instantiation Beyond E-Matching. SMT (2017)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI (2016)
Andrew Reynolds, Radu Iosif, Cristina Serban
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic. CoRR (2016)
Andrew Reynolds
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. Vampire@IJCAR (2016)
Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze
Efficient solving of string constraints for security analysis. HotSoS (2016)
Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD (2016)
Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King
A Decision Procedure for Separation Logic in SMT. ATVA (2016)
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48 (3) (2016)
Andrew Reynolds, Radu Iosif, Tim King
A Decision Procedure for Separation Logic in SMT. CoRR (2016)
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
Model Finding for Recursive Functions in SMT. IJCAR (2016)
Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR (2016)
Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR (2015)
Andrew Reynolds, Tim King, Viktor Kuncak
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR (2015)
Andrew Reynolds, Jasmin Christian Blanchette
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE (2015)
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR (2015)
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
On Deciding Local Theory Extensions via E-matching. CoRR (2015)
Andrew Reynolds, Viktor Kuncak
Induction for SMT Solvers. VMCAI (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) (2015)
Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies
Deciding Local Theory Extensions via E-matching. CAV (2) (2015)
Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
A tour of CVC4: How it works, and how to use it. FMCAD (2014)
Andrew Reynolds
Approaches for Synthesis Conjectures in an SMT Solver. CoRR (2014)
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV (2014)
Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura
Finding conflicting instances of quantified formulas in SMT. FMCAD (2014)
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli
SMT proof checking using a logical framework. Formal Methods Syst. Des. 42 (1) (2013)
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic
Finite Model Finding in SMT. CAV (2013)
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett
Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE (2013)
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang
LFSC for SMT Proofs: Work in Progress. PxTP (2012)
Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli
CVC4. CAV (2011)