He has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His research has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (including Amazon, Intel, General Electric, Facebook, Rockwell Collins, and United Technologies). His work has appeared in more than 120 peer-reviewed publications.

He has led the development of the award-winning Darwin theorem prover and the Kind 1 and Kind 2 model checkers. He has co-led the development of the widely used and award-winning CVC3, CVC4 and cvc5 SMT solvers. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He also co-led the development of StarExec, a cross community web-based service for the comparative evaluation of logic solvers.

He is an associate editor of the Journal of Automated Reasoning and a co-founder of the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of more than 90 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FroCoS, FTP, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15 and CADE-29.

He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community, and a CAV Conference award in 2021 for his role in the development of SMT. He has given invited talks or tutorials at CADE, CAV, ETAPS, FroCoS, HVC, NFM, NSV, SAT, TABLEAUX, VERIFY, VSTTE, and WoLLIC.