OSTRICH2: Solver for Complex String Constraints
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916901056151552 |
|---|---|
| author | Hague, Matthew Hu, Denghang Jeż, Artur Lin, Anthony W. Markgraf, Oliver Rümmer, Philipp Wu, Zhilin |
| author_facet | Hague, Matthew Hu, Denghang Jeż, Artur Lin, Anthony W. Markgraf, Oliver Rümmer, Philipp Wu, Zhilin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_14363 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | OSTRICH2: Solver for Complex String Constraints Hague, Matthew Hu, Denghang Jeż, Artur Lin, Anthony W. Markgraf, Oliver Rümmer, Philipp Wu, Zhilin Logic in Computer Science 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. |
| title | OSTRICH2: Solver for Complex String Constraints |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.14363 |