SMT is a branch of automatic reasoning concerned with determining the satisfiability of first-order formulas with respect to certain logical theories of interest. Its distinguishing feature is the use of specialized inference methods for each theory, and their incorporation into a general purpose deductive mechanism.
Thanks to their power and speed, SMT solvers are now used in a large and ever growing number of applications. They are most effective with problems reducible to the satisfiability of quantifier-free formulas. Many applications, however, require the use of quantified formulas as well, typically to provide axiomatic definitions of function or predicate symbols not included in the built-in theories. Unfortunately, combining effectively quantified queries and theories has proven to be one of the most challenging problems in automated deduction, which has led to the adoption of pragmatic but fairly limited approaches to deal with quantifiers in SMT.
This talks briefly overviews these approaches, based on heuristic instantiation. Then it presents a few promising novel techniques which instead rely of the internal construction of full candidate models for the input formulas in order to drive quantifier instantiation. Some of these model-based techniques have been implemented with significant initial success in the CVC4 SMT solver, jointly-developed with New York University.
Cesare Tinelli is a professor of Computer Science and collegiate scholar at the University of Iowa. He received a PhD in Computer Science from UIUC in 1999. His research interests include automated reasoning, formal methods, foundations of programming languages, and applications of logic in CS. He is an internationally renowned expert in Theorem Proving, Satisfiability Modulo Theories and their applications to automated verification. His research has appeared in several highly-ranked conferences and journals and funded by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, Rockwell Collins, and United Technologies).
He has led the development of the award winning Darwin theorem prover and the Kind model checker, and co-led the development of the widely used 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, and a coordinator of StarExec, a large NSF-funded public execution service for logic solvers.
He received an NSF CAREER award in 2003 and a Haifa Verification Conference award in 2010. He has given more than 50 invited talks and lectures worldwide including talks at CAV, HVC, NFM, TABLEAUX, VERIFY, and WoLLIC. He is an associate editor of the Journal of Automated Reasoning and a founder the SMT and the Midwest Verification Day workshop series. He has served in the program committee of numerous automated reasoning and formal methods conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS, and SMT. He was the PC chair of FroCoS'11 and will co-chair TACAS'15.
yano [atsymbol] cs.cmu.edu