An Efficient SMT Solver for String Constraints

by Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, Morgan Deters
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. Until recently, satisfiability solvers for strings were standalone tools that could reason only about fairly restricted fragments of the theory of strings and regular expressions such as, for instance, strings of bounded lengths. These solvers were 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 a rich theory of unbounded strings natively, without reduction to other problems. These techniques can be used to integrate string reasoning into general, multi-theory SMT solvers based on the DPLL(T) architecture. 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. This implementation makes CVC4 the first solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays and algebraic datatypes. 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.
Reference:
An Efficient SMT Solver for String Constraints (Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, Morgan Deters), In Formal Methods in System Design, Springer US, volume 48, 2016.
Bibtex Entry:
@article {LRT+16,
   url       = "http://www.cs.stanford.edu/~barrett/pubs/LRT+16.pdf",
   author    = "Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze and Cesare Tinelli and Clark Barrett and Morgan Deters",
   title     = "An Efficient {SMT} Solver for String Constraints",
   journal   = "Formal Methods in System Design",
   publisher = "Springer US",
   keywords  = "String solving; Satisfiability Modulo Theories; Automated Deduction",
   volume    = 48,
   number    = 3,
   pages     = "206--234",
   month     = jun,
   year      = 2016,
   issn      = "1572-8102",
   doi       = "10.1007/s10703-016-0247-6",
   category  = "Journal Articles",
   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.
Until recently, satisfiability solvers for strings were standalone tools 
that could reason only about fairly restricted fragments of the theory 
of strings and regular expressions such as, for instance, strings
of bounded lengths.
These solvers were 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 
a rich theory of unbounded strings natively, without reduction 
to other problems. 
These techniques can be used to integrate string reasoning into general, 
multi-theory SMT solvers based on the DPLL(T) architecture.
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.
This implementation makes CVC4 the first solver able to accept 
a rich set of mixed constraints over strings, integers, reals, arrays 
and algebraic datatypes.
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."
}

Fork me on GitHub