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.


Conference Papers

Workshop Papers

Journal Papers

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.



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

Program Committee Experience


Visualization of Floating point Invertibility Conditions

Contact Info