**I have moved to University of Iowa.**

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

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

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

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

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

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

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