Andrew Reynolds

I am a Research Scientist at the University of Iowa and one of main developers of the Satisfiability Modulo Theories (SMT) solver CVC5. I am part of the Computational Logic Center CLC at the University of Iowa. My current research interests include implementing techniques in SMT solvers for unbounded strings and regular expressions, proofs, quantified formulas and synthesis conjectures.

Publications

Conference Papers

Elizabeth Polgreen, Andrew Reynolds and Sanjit Seshia. Satisfiability and Synthesis Modulo Oracles, VMCAI 2022.
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning via Int-Blasting, VMCAI 2022.
Mikolas Janota, Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Fair and Adventurous Enumeration of Quantifier Instantiations, FMCAD 2021.
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Politeness and Stable Infiniteness: Stronger Together, CADE 2021.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Syntax-Guided Quantifier Instantiation, Best paper honorable mention, TACAS 2021.
Andrew Reynolds, Andres Noetzli, Clark Barrett, and Cesare Tinelli. Revisiting Reductions for Strings and Regular Expressions, FMCAD 2020.
Mohammed Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury and Cesare Tinelli. Syntax-Guided Synthesis of PLTL Formulas from Finite Traces, FMCAD 2020.
Andrew Reynolds, Andres Noetzli, Clark Barrett, and Cesare Tinelli. A Decision Procedure for String to Code Point Conversion, IJCAR 2020.
Andrew Reynolds, Haniel Barbosa, Daniel Larraz and Cesare Tinelli. Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis, IJCAR 2020.
Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli. Extending Enumerative Function Synthesis via SMT-Driven Classification, Best paper honorable mention, FMCAD 2019.
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Invertibility Conditions for Floating Point Formulas, CAV 2019.
Andrew Reynolds, Haniel Barbosa, Andres Noetzli, Clark Barrett, and Cesare Tinelli. CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis, CAV 2019 tool paper.
Andrew Reynolds, Andres Noetzli, Clark Barrett, and Cesare Tinelli. High-Level Abstractions for Simplifying Extended String Constraints in SMT, CAV 2019.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. Towards Bit-Width-Independent Proofs in SMT Solvers, CADE 2019.
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. Extending SMT Solvers to Higher-Order Logic, CADE 2019.
Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli. Syntax-Guided Rewrite Rule Enumeration for SMT Solvers, SAT 2019.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Solving Quantified Bit-Vectors using Invertibility Conditions, CAV 2018.
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett. Datatypes with Shared Selectors, IJCAR 2018.
Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting Enumerative Instantiation, TACAS 2018.
Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic and Clark Barrett. Designing Theory Solvers with Extensions, Invited paper, FroCoS 2017.
Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang and Cesare Tinelli. Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification, CAV 2017.
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds and Clark Barrett. SMTCoq: A Plug-in for Integrating SMT Solvers into Coq, CAV 2017, tool paper.
Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Relational Constraint Solving in SMT. CADE 2017.
Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Congruence Closure with Free Variables. TACAS 2017.
Andrew Reynolds, Radu Iosif, and Cristina Serban. Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of Separation Logic. VMCAI 2017.
Guy Katz, Clark Barrett, Liana Hadarean, Andrew Reynolds and Cesare Tinelli. Lazy Proofs for DPLL(T)-Based SMT Solvers. Best paper award, FMCAD 2016.
Andrew Reynolds, and Jasmin Christian Blanchette. A Decision Procedure for (Co)Datatypes in SMT Solvers. Sister conference best paper track, IJCAI 2016.
Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A Decision Procedure for Separation Logic in SMT. ATVA 2016.
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli. Model Finding for Recursive Functions in SMT. IJCAR 2016.
Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016.
Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, and Morgan Deters. Fine-Grained SMT proofs for the theory of fixed-width bit-vectors. LPAR 2015.
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCoS 2015.
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV 2015.
Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, and Thomas Wies. Deciding Local Theory Extensions via E-matching. CAV 2015.
Andrew Reynolds, and Jasmin Christian Blanchette. A Decision Procedure for (Co)Datatypes in SMT Solvers. CADE 2015.
Andrew Reynolds, and Viktor Kuncak. Induction for SMT Solvers. VMCAI 2015.
Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. Finding Conflicting Instances of Quantified Formulas in SMT. FMCAD 2014.
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Morgan Deters, and Clark Barrett. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV 2014.
Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstic. Finite Model Finding in SMT. CAV 2013.
Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark Barrett. Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE 2013.
Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. CAV 2011, tool paper.

Workshop Papers

Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett, and Cesare Tinelli. Rewrites for SMT Solvers using Syntax-Guided Enumeration (Work in Progress), SMT 2018.
Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. Higher-Order SMT Solving (Work in Progress), SMT 2018.
Andrew Reynolds, and Cesare Tinelli. SyGuS Techniques in the Core of an SMT Solver, Invited paper, SYNT 2017.
Andrew Reynolds. Challenges for Fast Synthesis Procedures in SMT, ARCADE 2017.
Andrew Reynolds. Conflicts, Models and Heuristics for Quantifier Instantiation in SMT, Invited paper, Vampire 2016.
Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew Reynolds, and Cesare Tinelli. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), HaTT 2016.
Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. Model Finding for Recursive Functions in SMT. SMT 2015.
Andrew Reynolds, Cesare Tinelli, and Leonardo de Moura. Finding Conflicting Instances of Quantified Formulas in SMT. QUANTIFY 2014.
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, and Ruoyu Zhang. LFSC for SMT Proofs: Work in Progress. PXTP 2012.
Andrew Reynolds, Cesare Tinelli, and Liana Hadarean.Certified Interpolant Generation for EUF. SMT 2011.
Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett. Comparing Proof Systems for Linear Real Arithmetic, SMT 2010.
Duckki Oe, Andrew Reynolds, and Aaron Stump. Fast and Flexible Proof Checking for SMT. SMT 2009.

Journal Papers

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. On Solving Quantified Bit-Vector Constraints Using Invertibility Conditions, FMSD 2021.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. Towards Satisfiability Modulo Parametric Bit-vectors, JAR 2021.
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, and Morgan Deters. Refutation-Based Synthesis in SMT. FMSD 2019.
Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Reasoning with Finite Sets and Cardinality Constraints in SMT. LMCS 2018.
Andrew Reynolds, Tim King, and Viktor Kuncak. Solving Quantified Linear Arithmetic by Counterexample-Guided Instantiation, FMSD 2017.
Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Constraint Solving for Finite Model Finding in SMT Solvers. TPLP 2017.
Andrew Reynolds, and Jasmin Christian Blanchette. A Decision Procedure for (Co)Datatypes in SMT Solvers. JAR 2017.
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. An Efficient SMT Solver for String Constraints. FMSD 2016.
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT Proof Checking Using a Logical Framework. FMSD 2013.

Technical Reports

I am one of the maintainers of the language standard for syntax-guided synthesis. The latest version 2.1 of the SyGuS language standard can be found here.

Andrew Reynolds. Approaches for Synthesis Conjectures in an SMT Solver, 2014.
Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett. From Declarative to Computational Proof Checking for LRA. Extended version of SMT 2010 paper.
Andrew Reynolds, Liana Hadarean, Cesare Tinelli, Yeting Ge, Aaron Stump, and Clark Barrett. CVC3 Proof Conversion to LFSC

Presentations

The Rise of SMT Solvers for String Constraints. Invited talk, TPSS 2021.
An Overview of Quantifier Instantiation in Modern SMT Solvers. Invited talk, Summer school on formal techniques 2021.
Syntax-Guided Synthesis in SMT: A View from Inside the Solver. Presented at Simons Institute workshop on Synthesis 2021.
A Decision Procedure for String to Code Point Conversion. Presented at IJCAR 2020.
Solving Verification Conditions Using SMT Solvers. Presented at MOVEP summer school 2020.
Quantifiers in SMT: A View from Inside the Solver. Presented at SRI seminar 2020.
Invertibility Conditions for Floating Point Formulas. Presented at CAV 2019.
Building Better SMT Solvers Using Syntax-Guided Synthesis. Presented at EPFL, 2019.
Towards Enumerative Invariant Synthesis in SMT Solvers. Invited talk, presented at NSV 2018.
Rewrites for SMT Solvers using Syntax-Guided Enumeration. Presented at SMT 2018.
An Introduction to SMT Solvers and Their Applications Colloquim talk, University of Iowa, 2017. (Part 2)
Fast and Slow Synthesis Procedures in SMT. Presented at Dagstuhl 2017.
Challenges for Fast Synthesis Procedures in SMT. Presented at ARCADE 2017.
Relational Constraint Solving in SMT. Presented at CADE 2017.
Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification. Presented at CAV 2017.
Quantifier Instantiation Beyond E-Matching. Invited talk, presented at SMT 2017.
SyGuS Techniques in the Core of an SMT Solver. Invited talk, presented at SYNT 2017.
SMT Solvers for Verification and Synthesis. Invited lecture, presented at VTSA summer school 2017. (Part 1) (Part 2)
Implementing Branch and Bound Algorithms in SMT. Presented at Two Sigma 2016.
A Decision Procedure for (Co)datatypes in SMT Solvers. Invited paper presentation, presented at IJCAI 2016.
Recent Advances in Instantiation-Based Techniques and Their Implementation in CVC4. Invited talk, presented at Vampire 2016.
Model Finding for Recursive Functions in SMT. Presented at IJCAR 2016.
Instantiation for Quantified Formulas in SMT: Techniques and Practical Aspects. Invited lecture, presented at SAT/SMT/AR summer school 2016.
Efficient Solving of String Constraints for Security Analysis. Poster presented at HotSoS 2016.
Using Instantiation-Based Methods for Quantifier Elimination in SMT. Presented at Dagstuhl seminar 2015.
A Taste of CVC4. Invited tutorial, copresented with Cesare Tinelli, FroCoS 2015.
A Decision Procedure for (Co)datatypes in SMT Solvers. Copresented with Jasmin Blanchette, CADE 2015.
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. Presented at CAV 2015.
Model Finding for Recursive Functions in SMT. Presented at SMT 2015, QUANTIFY 2015.
Satisfiability Modulo Theories: Beyond Decision Proceduces. Presented at Google 2015.
Synthesis by Quantifier Instantiation in CVC4. Presented at AVM 2015.
Using CVC4 for Proofs by Induction. Presented at 2nd Workshop for Automated Inductive Theorem Proving 2015, Verimag 2015.
Satisfiability Modulo Theories and DPLL(T). Presented at EPFL 2015.
Induction for SMT Solvers. Presented at VMCAI 2015.
Induction in CVC4. Presented at TU Munich 2014.
Finding Conflicting Instances of Quantified Formulas in SMT. Presented at FMCAD 2014.
A Tour of CVC4: How it Works, and how to Use it. Invited tutorial, copresented with Morgan Deters and Tim King, FMCAD 2014.
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. Presented at CAV 2014.
Finding Conflicting Instances of Quantified Formulas in SMT. Presented at CEA Paris, 2014, QUANTIFY 2014.
A DPLL(T) Theory Solver for Strings and Regular Expressions. Presented at EPFL 2014.
Design of Theory Solvers in CVC4. Presented at EPFL 2014.
Finite Model Finding in Satisfiability Modulo Theories. Presented at University of Iowa 2013.
Quantifier Instantiation Techniques for Finite Model Finding in SMT. Presented at CADE 2013.
Model-Based Reasoning About Quantified Formulas in CVC4. Presented at University of Iowa 2013, EPFL 2013.
Extending SMT to Quantified Formulas. Presented at University of Iowa, 2012.
(Condensed Version) Generating Small Counterexamples Using SMT. Presented at MVD 2012, New York University 2012.
Generating Small Counterexamples Using SMT. Presented at Intel Research, 2012.
LFSC for SMT Proofs: Works in Process. Presented at PxTP, 2012.
Finite Model Finding for SMT. Presented at Intel and Microsoft Research, 2012.
Fast and Flexible Proof Checking with LFSC.. Presented at University of Iowa 2011.
A Counterexample-Based Approach for Quantifier Instantiation. Presented at New York University 2011, MVD 2011.
Certified Interpolant Generation for EUF. Presented at SMT 2011.
Comparing Proof Systems for Linear Real Arithmetic. Copresented with Liana Hadarean, SMT 2010. Also presented at MVD 2010.
Fast and Flexible Proof Checking for SMT. Copresented with Duckki Oe, SMT 2009 and MVD 2009.

Competitions

My work in CVC4 has been entered in the following competitions.

SMT Comp 2021

Won 7 of 12 divisions with quantified formulas.
Won Quantifier-free strings division.

CASC 28
SMT Comp 2020

Won 25 of 33 logics with quantified formulas.
Won Quantifier-free strings logics (QF_S and QF_SLIA).
Won Non-linear integer arithmetic logic.

CASC J10
SyGuS Comp 2019

Won, General track.
Won, Programming by Examples Strings and Bit-Vectors track.
Won, Invariant Synthesis track.

SMT Comp 2019

Won 10 of 23 logics with quantified formulas.
Won QF_S (strings) logic.
Won QF_NIA logic, largest contribution.

CASC 27
SyGuS Comp 2018

Won, General track.
Won (tied), Conditional Linear Integer Arithmetic track.
Won, Programming by Examples Strings and Bit-Vectors track.
Placed 2nd in the Invariant Synthesis track.

SMT Comp 2018

Won 16 of 19 logics with quantified formulas, including quantified bit-vectors (BV).
Outperformed all known solvers in 8 of 19 logics with quantified formulas.
Won QF_NIA division.

CASC J9
SyGuS Comp 2017

Won, Conditional Linear Integer Arithmetic track.
Won, Programming by Examples Strings track.
Placed 2nd in the General and Invariant Synthesis tracks.

SMT Comp 2017

Won 9 of 15 logics with quantified formulas (ALIA, AUFLIA, LIA, LRA, NIA, UFBV, UFIDL, UFLIA, UFLRA).
Outperformed all known solvers in 3 of 15 logics with quantified formulas.
Won QF_NIA division.

CASC 26

Placed 4th in first-order theorems division, only behind versions of E and Vampire.

SyGuS Comp 2016

Won, Conditional Linear Integer Arithmetic track.
Placed 2nd in the General and Invariant Synthesis tracks.

SMT Comp 2016

Won 8 of 15 logics with quantified formulas.
Outperformed all known solvers in 5 of 15 logics with quantified formulas.

CASC J8
SyGuS Comp 2015

Won, General and Conditional Linear Integer Arithmetic tracks.

SMT Comp 2015

Won 8 of 9 logics with quantified formulas.
Outperformed all known solvers in 5 of 9 logics with quantified formulas.

CASC 25

Won, typed first-order non-theorems division.
Placed 2nd in typed first-order theorems division.

SMT Comp 2014

Won 8 of 9 logics with quantified formulas.
Outperformed all known solvers in 4 of 9 logics with quantified formulas.

CASC J7

Won, typed first-order theorems division.

CASC 24

Placed 3rd in the non-theorem division, earned the CASC 24 special mention award.

SMT Comp 2012

Won, AUFLIRA division.

CASC J6

Program Committee Experience

Board of trustees, International Conference on Automated Deduction (CADE), 2017-.
Co-chair of Artifact Evaluation, TACAS 2022.
Steering committee, International Workshop on Satisfiability Modulo Theories (SMT), 2017-2021.
PC Member CADE 2021, SMT 2021, FMCAD 2021, ATVA 2021, SoCS 2021, F-IDE 2021, FroCoS 2021, ARCADE 2021.
Workshop chair, IJCAR 2020.
PC Member IJCAR 2020, LPAR 2020, IWIL 2020, SMT 2020.
Co-organizer, SyGuS Comp 2019, the 6th edition of the syntax-guided synthesis competition.
PC Member CADE 2019.
Co-organizer, 2018 FMCAD Student Forum.
Co-organizer, SSA 2018, 2018 Summer School on SAT, SMT and Automated Reasoning.
Co-organizer, VDMW 2018, Verification and Deduction Mentoring Workshop.
Co-organizer, ICMS 2018, Quantified Reasoning session.
PC Member SMT 2018, AVOCS 2018, PAAR 2018, SETS 2018.
PC Member, artifact evaluation, CAV 2018.
PC Member PXTP 2017, IWIL 2017.
PC Member, artifact evaluation, CAV 2017.
PC Member PAAR 2016, SMT 2016, TAP 2016
PC Member, artifact evaluation, POPL 2016.
Co-chair of Workshops, Tutorials, and Competitions, CADE 2015, 25th edition of the International Conference on Automated Deduction.
PC Member CADE 2015, TAP 2015, SMT 2015, IWIL 2015
PC Member, artifact evaluation, CAV 2015.
PC Member IWIL 2014.

Other

Visualization of Floating point Invertibility Conditions

Contact Info

E-mail: andrew.j.reynolds@gmail.com