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. My current research interests include implementing techniques in SMT solvers for unbounded strings and regular expressions, first-order quantified formulas and synthesis conjectures.

Publications

Conference Papers

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.
Baolo 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-Schönfinkel-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. 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

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, Tim King, and Viktor Kuncak. An Instantiation-Based Approach for Solving Quantified Linear Arithmetic, 2015.
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

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:

CASC J8

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 (ALIA, AUFLIA, LIA, LRA, UF, UFBV, UFIDL, UFLIA).
Outperformed all known solvers in 5 of 15 divisions with quantified formulas.

CASC 25

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

SyGuS Comp 2015

Won, General and Conditional Linear Integer Arithmetic tracks.

SMT Comp 2015

Won 8 of 9 divisions with quantified formulas (ALIA, AUFLIA, AUFLIRA, LIA, LRA, UF, UFIDL, UFLIA).
Outperformed all known solvers in 5 of 9 divisions with quantified formulas.

CASC J7

Won, 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 24

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

CASC J6
SMT Comp 2012

Won, AUFLIRA division.

Program Committee Experience

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