I work on Satisfiability Modulo Theories (SMT). In my research, I do both theoretical and practical work. On the theory side, I focus on theory combination, as well as correctness arguments for SMT algorithms. On the practical side, I am a member of the cvc5 and smt-switch team, and implement decision procedures using these tools.