OSTRICH2: Solver for Complex String Constraints

Matthew Hague; Denghang Hu; Artur Jeż; Anthony Lin; Oliver Markgraf; Philipp Rümmer; Zhilin Wu

OSTRICH2: Solver for Complex String Constraints

Matthew Hague, Denghang Hu, Artur Jeż, Anthony Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

8 Downloads (Pure)

Abstract

We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

Original language	English
Title of host publication	Formal Methods in Computer-Aided Design (FMCAD)
Publication status	Accepted/In press - 1 Jul 2025

Keywords

satisfiability modulo theories
strings
smt-lib
constraints
verification
formal methods

Access to Document

OSTRICH2: Solver for Complex String ConstraintsAccepted author manuscript, 426 KB

String Constraint Solving with Real-World Regular Expressions
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/07/19 → 30/06/22
Project: Research

Cite this

@inbook{d42432aebbf240c196535d13e1ae859b,

title = "OSTRICH2: Solver for Complex String Constraints",

abstract = "We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.",

keywords = "satisfiability modulo theories, strings, smt-lib, constraints, verification, formal methods",

author = "Matthew Hague and Denghang Hu and Artur Je{\.z} and Anthony Lin and Oliver Markgraf and Philipp R{\"u}mmer and Zhilin Wu",

year = "2025",

month = jul,

day = "1",

language = "English",

booktitle = "Formal Methods in Computer-Aided Design (FMCAD)",

}

TY - CHAP

T1 - OSTRICH2: Solver for Complex String Constraints

AU - Hague, Matthew

AU - Hu, Denghang

AU - Jeż, Artur

AU - Lin, Anthony

AU - Markgraf, Oliver

AU - Rümmer, Philipp

AU - Wu, Zhilin

PY - 2025/7/1

Y1 - 2025/7/1

N2 - We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

AB - We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look‐around assertions and capture groups) and handling of user‐defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

KW - satisfiability modulo theories

KW - strings

KW - smt-lib

KW - constraints

KW - verification

KW - formal methods

M3 - Chapter (peer-reviewed)

BT - Formal Methods in Computer-Aided Design (FMCAD)

ER -

OSTRICH2: Solver for Complex String Constraints

Abstract

Keywords

Access to Document

Projects

String Constraint Solving with Real-World Regular Expressions

Cite this