# OSTRICH2: Solver for Complex String Constraints

arXiv: https://arxiv.org/abs/2506.14363 · HTML: https://mlsanity.com/paper/2506.14363/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jun 2025.

## Built on by (most cited first, 1 of 1)

- [Neurosymbolic Characterization for Reliable Access Control Policy Analysis](https://mlsanity.com/paper/2510.20692/) (2025)

## Abstract (arXiv)

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.