Andrew Reynolds

I am a Research Scientist at the University of Iowa and one of main developers of the Satisfiability Modulo Theories (SMT) solver CVC4. 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, first-order quantified formulas and synthesis conjectures.

Teaching

CS 5810, Formal Methods in Software Engineering, Fall 2019.

Publications

Conference Papers

Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli. Extending Enumerative Function Synthesis via SMT-Driven Classification, 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

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, Viktor Kuncak, Cesare Tinelli, Clark Barrett, and Morgan Deters. Refutation-Based Synthesis in SMT. FMSD 2017.
Andrew Reynolds, and Jasmin Christian Blanchette. A Decision Procedure for (Co)Datatypes in SMT Solvers. JAR 2016.
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

Baolo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Relational Constraint Solving in SMT. Extended version of CADE 2017 paper.
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

Dissertation

Finite Model Finding in Satisfiability Modulo Theories. Accepted University of Iowa, December 2013.

Presentations

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.

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 divisions with quantified formulas.
Won QF_S (strings) division.
Won QF_NIA division, 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 divisions with quantified formulas, including quantified bit-vectors (BV).
Outperformed all known solvers in 8 of 19 divisions 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 divisions with quantified formulas (ALIA, AUFLIA, LIA, LRA, NIA, UFBV, UFIDL, UFLIA, UFLRA).
Outperformed all known solvers in 3 of 15 divisions 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 divisions with quantified formulas.
Outperformed all known solvers in 5 of 15 divisions with quantified formulas.

CASC J8
SyGuS Comp 2015

Won, General and Conditional Linear Integer Arithmetic tracks.

SMT Comp 2015

Won 8 of 9 divisions with quantified formulas.
Outperformed all known solvers in 5 of 9 divisions 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 divisions with quantified formulas.
Outperformed all known solvers in 4 of 9 divisions 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

Steering committee, International Workshop on Satisfiability Modulo Theories (SMT), 2017-.
Board of trustees, International Conference on Automated Deduction (CADE), 2017-.
Co-organizer, SyGuS Comp 2019, the 6th edition of the syntax-guided synthesis competition.
PC Member CADE 2019, 27th edition of the International Conference on Automated Deduction.
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, 16th International Workshop on Satisfiability Modulo Theories.
PC Member, artifact evaluation, CAV 2018.
PC Member AVOCS 2018, 18th International Workshop on Automated Verification of Critical Systems.
PC Member PAAR 2018, 6th Workshop on Practical Aspects of Automated Reasoning.
PC Member SETS 2018, 3th Workshop on Sets and Tools.
PC Member PXTP 2017, 5th Workshop on Proof Exchange for Theorem Proving.
PC Member, artifact evaluation, CAV 2017.
PC Member IWIL 2017, 11th International Workshop on the Implementation of Logics.
PC Member PAAR 2016, 5th Workshop on Practical Aspects of Automated Reasoning.
PC Member SMT 2016, 14th International Workshop on Satisfiability Modulo Theories.
PC Member TAP 2016, 10th International Conference on Tests and Proofs.
PC Member, artifact evaluation, POPL 2016.
PC Member IWIL 2015, 11th International Workshop on the Implementation of Logics.
Co-chair of Workshops, Tutorials, and Competitions, CADE 2015, 25th edition of the International Conference on Automated Deduction.
PC Member SMT 2015, 13th International Workshop on Satisfiability Modulo Theories.
PC Member TAP 2015, 9th International Conference on Tests and Proofs.
PC Member CADE 2015, 25th edition of the International Conference on Automated Deduction.
PC Member, artifact evaluation, CAV 2015.
PC Member IWIL 2014, 10th International Workshop on the Implementation of Logics.

Contact Info

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