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.
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning via Int-Blasting, VMCAI 2022.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Syntax-Guided Quantifier Instantiation, Best paper honorable mention, TACAS 2021.
Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. CAV 2011, tool paper.
Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, and Ruoyu Zhang. LFSC for SMT Proofs: Work in Progress. PXTP 2012.
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.