Andrew Reynolds

I am a Post-Doc at the LARA group at EPFL in Lausanne, Switzerland, working with Viktor Kuncak. My research focus is on various aspects of Satisfiability Modulo Theories, including quantified formulas, decision procedures, and proof checking. I am the primary developer of the module for handling quantified formulas in the SMT solver CVC4. My current focus is developing new techniques for handling quantified formulas within SMT solvers, including heuristic E-matching, finite model finding, model-based instantiation, methods for automating proofs by induction, and approaches for synthesis conjectures.

Publications

Papers

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, Jasmin Christian Blanchette, and Cesare Tinelli. Model Finding for Recursive Functions in SMT. SMT 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, and Leonardo de Moura. Finding Conflicting Instances of Quantified Formulas in SMT. QUANTIFY 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.
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, and Ruoyu Zhang. LFSC for SMT Proofs: Work in Progress. PXTP 2012.
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT Proof Checking Using a Logical Framework. FMSD journal.
Andrew Reynolds, Cesare Tinelli, and Liana Hadarean.Certified Interpolant Generation for EUF. SMT 2011.
Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. CAV tool paper 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.

Technical Reports

Andrew Reynolds, Tim King, and Viktor Kuncak. An Instantiation-Based Approach for Solving Quantified Linear Arithmetic, 2015.
Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. Model Finding for Recursive Functions in SMT. Extended version of SMT 2015 paper.
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. On Counterexample-Guided Quantifier Instantiation for Synthesis in CVC4. Extended version of CAV 2015 paper.
Andrew Reynolds, and Jasmin Christian Blanchette. A Decision Procedure for (Co)Datatypes in SMT Solvers. Extended version of CADE 2015 paper.
Andrew Reynolds. Approaches for Synthesis Conjectures in an SMT Solver, 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. Extended version of CAV 2014 paper.
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

Using Instantiation-Based Methods for Quantifier Elimination in SMT. Dagstuhl 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. 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 25

Won, typed first-order non-theorems division.
Placed 2nd in typed first-order theorems division.
Placed 5th in first-order theorems division, only behind versions of E and Vampire.

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 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