CS Talk
Nestan Tsiskaridze
Title: An Efficient SMT Based Solver for String and Regular Expression Constraints
Host: Ruzica Piskac
Abstract: Nowadays, an increasing number of applications in verification and security rely on automated solvers which can decide the satisfiability of constraints over various sets of data types, including character strings. The quest on automated solver that can handle string constraints is very high in security analysis. However, most of the existing string solvers today are standalone tools that can reason only about small fragments of string constraints. These solvers are based on reductions to the satisfiability problems over other data types, such as bit-vectors, or to decision problems over automata. In this talk will be presented a new algorithm that allows reasoning on quantifier-free constraints over a theory of unbounded strings, length constraints, regular expression membership, and common string manipulating functions, directly without reducing to other problems. The algorithm is incorporated into the state-of-the-art SMT solver CVC4 as a plugged-in theory solver for strings and this way expands CVC4’s already large set of built-in theories. This work makes CVC4 the first SMT solver that is able to handle a rich set of mixed constraints over strings, integers/reals, bit-vectors, arrays, and other data types. As experimental results show, on string problems, the new approach is highly effective – it outperforms other existing specialized string solvers in terms of correctness, precision, and run time, when compared on a comparable input language.
Bio: I obtained my PhD from the University of Manchester at the Department of Computer Science under the supervision of Prof. Andrei Voronkov (the home of the World Cup winning automated theorem prover — Vampire, by Prof. Andrei Voronkov et al.).
My PhD research was related to the development of new methods for solving SMT problems with theories of linear real and integer arithmetics. The research introduced the Conflict Driven Clause Learning (CDCL)-like procedures into the area of Linear Programming. The thesis presented a new method for Linear Programming - the Conflict Resolution method.
After graduating from PhD I moved to Princeton University and joined Prof. Sharad Malik’s group at the Department of Electrical Engineering for my postdoctoral position (the home of an CDCL SAT solver — Chaff, by Prof. Sh. Malik et al.). At Princeton, I was working in a team on a DARPA IRIS project, which concerned with reverse engineering of digital, analog and mixed-signal integrated circuits (IC) to determine their integrity and reliability for use in sensitive applications. The work involved development of algorithms for automated reverse engineering of ICs, starting from an unstructured netlist and resulting in a high-level netlist with compound components. My later work at Princeton concerned solving the All-SAT problem using minimal blocking clauses.
Since July 2013 I work as a postdoctoral research scholar and a visiting assistant professor at the University of Iowa in the Department of Computer Science. I am currently working with Prof. Cesare Tinelli (the home of an SMT solver — CVC4, by Prof. C. Tinelli et al.) on developing new Satisfiability Modulo Theories (SMT) solving techniques to aid checking of software security properties, and on enhancing the CVC4 SMT solver with the new techniques. Namely we’ve been working on enhancing CVC4 with a new string solver that handles equalities, membership constraints and linear length constraints over the strings.