TY - JOUR
T1 - An efficient SMT solver for string constraints
AU - Liang, Tianyi
AU - Reynolds, Andrew
AU - Tsiskaridze, Nestan
AU - Tinelli, Cesare
AU - Barrett, Clark
AU - Deters, Morgan
N1 - Publisher Copyright:
© 2016, Springer Science+Business Media New York.
PY - 2016/6/1
Y1 - 2016/6/1
N2 - 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 diverse 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 (e.g., 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 common DPLL(T) architecture. We have implemented them in our SMT solver cvc4, expanding its already large set of built-in theories to include 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, on pure string problems cvc4 is highly competitive with specialized string solvers accepting a comparable input language.
AB - 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 diverse 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 (e.g., 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 common DPLL(T) architecture. We have implemented them in our SMT solver cvc4, expanding its already large set of built-in theories to include 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, on pure string problems cvc4 is highly competitive with specialized string solvers accepting a comparable input language.
KW - Automated deduction
KW - Satisfiability modulo theories
KW - String solving
UR - http://www.scopus.com/inward/record.url?scp=84962745529&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84962745529&partnerID=8YFLogxK
U2 - 10.1007/s10703-016-0247-6
DO - 10.1007/s10703-016-0247-6
M3 - Article
AN - SCOPUS:84962745529
SN - 0925-9856
VL - 48
SP - 206
EP - 234
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 3
ER -