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 - Funding Information:
We thank the developers of z 3 -str for their technical support in using their tool and several clarifications on it, as well as for their prompt response to our inquiries. We also express our gratitude to the developers of the StarExec service for their assistance and for implementing additional features we requested while running our experimental evaluation on the service. Finally, we thank the anonymous reviewers for their supportive comments and for their valuable suggestions on improving the paper’s presentation. The work described here was partially funded by NSF Grants #1228765 and #1228768. The second author was also supported in part by the European Research Council (ERC) Project Implicit Programming.
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 -