Andrew Reynolds

According to our database, Andrew Reynolds authored at least 88 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Verifying SQL queries using theories of tables and relations.

Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

Satisfiability Modulo Theories: A Beginner's Tutorial.

Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar

Proceedings of the Formal Methods - 26th International Symposium, 2024

The SemGuS Toolkit.

Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Combining Stable Infiniteness and (Strong) Politeness.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., December, 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, Cesare Tinelli, Yoni Zohar

Commun. ACM, October, 2023

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., September, 2023

Synthesising Programs with Non-trivial Constants.

Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli

J. Autom. Reason., June, 2023

The SyGuS Language Standard Version 2.1.

Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, Abhishek Udupa

CoRR, 2023

Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Selecting Quantifiers for Instantiation in SMT.

Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

An Interactive SMT Tactic in Coq using Abductive Reasoning.

Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Partitioning Strategies for Distributed SMT Solving.

Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett

Proceedings of the Formal Methods in Computer-Aided Design, 2023

A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery.

Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

Bit-Precise Reasoning via Int-Blasting.

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

Satisfiability and Synthesis Modulo Oracles.

Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description).

Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

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

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact).

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Dataset, February, 2021

Towards Satisfiability Modulo Parametric Bit-vectors.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., 2021

On solving quantified bit-vector constraints using invertibility conditions.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Formal Methods Syst. Des., 2021

lazybvtoint at the SMT Competition 2020.

Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett

CoRR, 2021

Syntax-Guided Quantifier Instantiation.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Characteristic Subsets of SMT-LIB Benchmarks.

Jan Jakubuv, Mikolás Janota, Andrew Reynolds

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

Fair and Adventurous Enumeration of Quantifier Instantiations.

Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Formal Methods in Computer Aided Design, 2021

Politeness and Stable Infiniteness: Stronger Together.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Reductions for Strings and Regular Expressions Revisited.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces.

M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

A Decision Procedure for String to Code Point Conversion.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.

Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Refutation-based synthesis in SMT.

Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters

Formal Methods Syst. Des., 2019

CVC4SY for SyGuS-COMP 2019.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

CoRR, 2019

SL-COMP: Competition of Solvers for Separation Logic.

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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Extending enumerative function synthesis via SMT-driven classification.

Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

High-Level Abstractions for Simplifying Extended String Constraints in SMT.

Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Invertibility Conditions for Floating-Point Formulas.

Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Deduction - CADE 27, 2019

Extending SMT Solvers to Higher-Order Logic.

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Reasoning with Finite Sets and Cardinality Constraints in SMT.

Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli

Log. Methods Comput. Sci., 2018

CVC4 at the SMT Competition 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

CoRR, 2018

Revisiting Enumerative Instantiation.

Andrew Reynolds, Haniel Barbosa, Pascal Fontaine

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

The FMCAD 2018 Graduate Student Forum.

Dejan Jovanovic, Andrew Reynolds

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Solving Quantified Bit-Vectors Using Invertibility Conditions.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Datatypes with Shared Selectors.

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Constraint solving for finite model finding in SMT solvers.

Andrew Reynolds, Cesare Tinelli, Clark W. Barrett

Theory Pract. Log. Program., 2017

A Decision Procedure for (Co)datatypes in SMT Solvers.

Andrew Reynolds, Jasmin Christian Blanchette

J. Autom. Reason., 2017

Solving quantified linear arithmetic by counterexample-guided instantiation.

Andrew Reynolds, Tim King, Viktor Kuncak

Formal Methods Syst. Des., 2017

SyGuS Techniques in the Core of an SMT Solver.

Andrew Reynolds, Cesare Tinelli

Proceedings of the Proceedings Sixth Workshop on Synthesis, 2017

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic.

Andrew Reynolds, Radu Iosif, Cristina Serban

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Congruence Closure with Free Variables.

Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Quantifier Instantiation Beyond E-Matching.

Andrew Reynolds

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Designing Theory Solvers with Extensions.

Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification.

Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Challenges for Fast Synthesis Procedures in SMT.

Andrew Reynolds

Proceedings of the ARCADE 2017, 2017

Relational Constraint Solving in SMT.

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Deduction - CADE 26, 2017

2016

An efficient SMT solver for string constraints.

Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters

Formal Methods Syst. Des., 2016

Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic.

Andrew Reynolds, Radu Iosif, Cristina Serban

CoRR, 2016

A Decision Procedure for Separation Logic in SMT.

Andrew Reynolds, Radu Iosif, Tim King

CoRR, 2016

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).

Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

Efficient solving of string constraints for security analysis.

Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze

Proceedings of the Symposium and Bootcamp on the Science of Security, 2016

Lazy proofs for DPLL(T)-based SMT solvers.

Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Model Finding for Recursive Functions in SMT.

Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

Conflicts, Models and Heuristics for Quantifier Instantiation in SMT.

Andrew Reynolds

Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT.

Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

A Decision Procedure for Separation Logic in SMT.

Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4.

Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli

CoRR, 2015

An Instantiation-Based Approach for Solving Quantified Linear Arithmetic.

Andrew Reynolds, Tim King, Viktor Kuncak

CoRR, 2015

Induction for SMT Solvers.

Andrew Reynolds, Viktor Kuncak

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.

Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings.

Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.

Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Deciding Local Theory Extensions via E-matching.

Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Approaches for Synthesis Conjectures in an SMT Solver.

Andrew Reynolds

CoRR, 2014

Finding conflicting instances of quantified formulas in SMT.

Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A tour of CVC4: How it works, and how to use it.

Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli

Proceedings of the Formal Methods in Computer-Aided Design, 2014

A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.

Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

SMT proof checking using a logical framework.

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli

Formal Methods Syst. Des., 2013

Finite Model Finding in SMT.

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Quantifier Instantiation Techniques for Finite Model Finding in SMT.

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett

Proceedings of the Automated Deduction - CADE-24, 2013

2012

LFSC for SMT Proofs: Work in Progress.

Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

2011

CVC4.

Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011