“An Efficient SMT Solver for String Constraints” by Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. Formal Methods in System Design, vol. 48, no. 3, June 2016, pp. 206-234, Springer US.
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.
Keywords: String solving; Satisfiability Modulo Theories; Automated Deduction
BibTeX entry:
@article{LRT+16,
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},
volume = {48},
number = {3},
pages = {206--234},
publisher = {Springer US},
month = jun,
year = {2016},
issn = {1572-8102},
doi = {10.1007/s10703-016-0247-6},
url = {http://theory.stanford.edu/~barrett/pubs/LRT+16.pdf}
}
(This webpage was created with bibtex2web.)