Cesare Tinelli received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is a F. Wendell Miller Professor at the University of Iowa. His research interests include automated reasoning, formal methods, software verification, foundations of programming languages, and applications of logic in computer science. 

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 (Amazon, Intel, General Electric, Facebook, Rockwell Collins, and United Technologies). 
His work has appeared in more than 80 refereed publications, including articles in such journals as Artificial Intelligence, Information and Computation, Formal Methods in System Design, the Journal of the ACM, the Journal of the Automated Reasoning, Logical Methods in Computer Science, Theoretical Computer Science, and Theory and Practice of Logic Programming.

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 and CVC4 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-leads 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 80 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15. 

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, and a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community. He has given invited talks or tutorials at CADE, CAV, ETAPS, FroCoS, HVC, NFM, NSV, TABLEAUX, VERIFY, VSTTE, and WoLLIC.