Cesare Tinelli is a professor of Computer Science and collegiate scholar at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. 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 Theory (SMT), a field he helped establish through his research and service activities. He leads the development of the Kind SMT-based model checker, and co-leads the development of the widely usedCVC4 SMT solver. He is also a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. His research has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, Rockwell Collins, and United Technologies). He received an NSF CAREER award in 2003 and a Haifa Verification Conference award in 2010. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of numerous 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 will co-chair TACAS’15.