Round Table: Cesare Tinelli - A Taste of Satisfiability Modulo Theories (SMT)
Pizza and sodas provided on a first-come first-served basis.
Please RSVP to firstname.lastname@example.org
Many problems in computer science can be reduced to checking the satisfiability of a formula in some formal logic. A large subclass of these problems can be naturally formulated as the problem of checking the satisfiability of a first-order formula with respect to, or modulo, some logical theory T of interest. Satisfiability Modulo Theories (SMT) is characterized by the use of inference methods that are highly specialized for each theory T. These methods can be implemented in solvers that are more efficient in practice than general-purpose automated reasoners. SMT solvers have been used successfully in several application areas, such as hardware and software verification, automated test case generation, security, and planning.
This talk will give an overview of SMT and its applications, and describe a few examples with the aid of the CVC4 solver. CVC4 is a widely used open-source SMT solver, jointly developed at New York University and the University of Iowa that supports a rich set of theories including the theory of arrays, bit vectors, linear integer and real arithmetic, algebraic data types, and strings.
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.