 |
Professor Cesare Tinelli |
CLASS LECTURE I: A Taste of SMT
Abstract:
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.
CLASS LECTURE II: An Efficient Solver for string and regular expression constraints
Abstract: An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a rich set of data types that includes character strings. Unfortunately, most string solvers today are standalone tools that can reason only about (some fragment) of the theory of strings and regular expressions, sometimes with strong restrictions on the expressiveness of their input language. These solvers are based on reductions to satisfiability problems over other data types, such as bit vectors, or to automata decision problems. We present a set of algebraic techniques for solving constraints over the theory of unbounded strings natively, without a reduction to other problems. These techniques can be used to integrate string reasoning into general solvers for satisfiability modulo theories (SMT). We have implemented them in our SMT solver CVC4 to expand its already large set of built-in theories to a theory of strings with concatenation, length, and membership in regular languages. Our initial experimental results show that, in addition, over pure string problems, CVC4 is highly competitive with specialized string solvers with a comparable input language
Biographical information:
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 2
SMT-based model checker, and co-leads the development of the widely used
CVC4 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.