An Efficient Solver for string and regular expression constraints
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. Until recently, available string solvers were standalone tools that could 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 were based on reductions to satisfiability problems over other data types, such as bit vectors, or to automata decision problems. In this talk, 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 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.
Speaker Details
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 revolve around automated reasoning and formal methods. He has done seminal work 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 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 a co-chair of TACAS’15.
- Date:
- Speakers:
- Cesare Tinelli
- Affiliation:
- University of Iowa
-
-
Jeff Running
-
