An efficient SMT solver for string constraints

Tianyi Liang; Andrew Reynolds; Nestan Tsiskaridze; Cesare Tinelli; Clark Barrett; Morgan Deters

doi:10.1007/s10703-016-0247-6

Back

An efficient SMT solver for string constraints

Journal article

Peer reviewed

An efficient SMT solver for string constraints

Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett and Morgan Deters

Formal methods in system design, Vol.48(3), pp.206-234

06/2016

DOI: 10.1007/s10703-016-0247-6

View Online

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 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.

String solving

03B20

03B10

03B22

03B70

Software Engineering/Programming and Operating Systems

Satisfiability modulo theories

Engineering

Automated deduction

Computer-Aided Engineering (CAD, CAE) and Design

Circuits and Systems

68Q60

03B25

Electrical Engineering

Details

Title: Subtitle: An efficient SMT solver for string constraints
Creators: Tianyi Liang - Two Sigma Investments New York USA
Andrew Reynolds - Department of Computer Science The University of Iowa Iowa USA
Nestan Tsiskaridze - Department of Computer Science The University of Iowa Iowa USA
Cesare Tinelli - Department of Computer Science The University of Iowa Iowa USA
Clark Barrett - Department of Computer Science New York University New York USA
Morgan Deters - Department of Computer Science New York University New York USA
Contributors: Armin Biere (Editor)
Roderick Bloem (Editor)
Resource Type: Journal article
Publication Details: Formal methods in system design, Vol.48(3), pp.206-234
DOI: 10.1007/s10703-016-0247-6
ISSN: 0925-9856
eISSN: 1572-8102
Publisher: Springer US; New York
Grant note: 1228768 / Directorate for Computer and Information Science and Engineering (http://dx.doi.org/10.13039/100000083) 1228765 / National Science Foundation (http://dx.doi.org/10.13039/100000001)
Language: English
Date published: 06/2016
Academic Unit: Computer Science
Record Identifier: 9984002590602771

Metrics

44 Record Views

41 Times Cited - Web of Science