An efficient SMT solver for string constraints

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

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)1-29
Number of pages29
JournalFormal Methods in System Design
DOIs
StateAccepted/In press - Apr 5 2016

Fingerprint

Surface mount technology
Strings
Formal languages
Constraint Solving
Regular Expressions
Concatenation
Regular Languages
Satisfiability Problem
Decision problem
Large Set
Automata
Fragment
Reasoning
Integrate
Integer

Keywords

  • Automated deduction
  • Satisfiability modulo theories
  • String solving

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Theoretical Computer Science

Cite this

Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., & Deters, M. (Accepted/In press). An efficient SMT solver for string constraints. Formal Methods in System Design, 1-29. https://doi.org/10.1007/s10703-016-0247-6

An efficient SMT solver for string constraints. / Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan.

In: Formal Methods in System Design, 05.04.2016, p. 1-29.

Research output: Contribution to journalArticle

Liang, T, Reynolds, A, Tsiskaridze, N, Tinelli, C, Barrett, C & Deters, M 2016, 'An efficient SMT solver for string constraints', Formal Methods in System Design, pp. 1-29. https://doi.org/10.1007/s10703-016-0247-6
Liang T, Reynolds A, Tsiskaridze N, Tinelli C, Barrett C, Deters M. An efficient SMT solver for string constraints. Formal Methods in System Design. 2016 Apr 5;1-29. https://doi.org/10.1007/s10703-016-0247-6
Liang, Tianyi ; Reynolds, Andrew ; Tsiskaridze, Nestan ; Tinelli, Cesare ; Barrett, Clark ; Deters, Morgan. / An efficient SMT solver for string constraints. In: Formal Methods in System Design. 2016 ; pp. 1-29.
@article{53737f8d941d458ba0b4d9f63d0cc150,
title = "An efficient SMT solver for string constraints",
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.",
keywords = "Automated deduction, Satisfiability modulo theories, String solving",
author = "Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze and Cesare Tinelli and Clark Barrett and Morgan Deters",
year = "2016",
month = "4",
day = "5",
doi = "10.1007/s10703-016-0247-6",
language = "English (US)",
pages = "1--29",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",

}

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

PY - 2016/4/5

Y1 - 2016/4/5

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

SP - 1

EP - 29

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

ER -