Publication detail

Z3-Noodler: An Automata-based String Solver

HAVLENA, V. CHOCHOLATÝ, D. SÍČ, J. HOLÍK, L. LENGÁL, O. CHEN, Y.

Original Title

Z3-Noodler: An Automata-based String Solver

Type

article in a collection out of WoS and Scopus

Language

English

Original Abstract

Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows that Z3-Noodler is a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.

Keywords

String solving, finite automata, SMT solving

Authors

HAVLENA, V.; CHOCHOLATÝ, D.; SÍČ, J.; HOLÍK, L.; LENGÁL, O.; CHEN, Y.

Released

4. 4. 2024

Publisher

Springer Verlag

Location

Luxembourgh

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

14570

State

Federal Republic of Germany

Pages from

24

Pages to

33

Pages count

10

URL

https://link.springer.com/chapter/10.1007/978-3-031-57246-3_2

BibTex

@inproceedings{BUT188550,
  author="Vojtěch {Havlena} and David {Chocholatý} and Juraj {Síč} and Lukáš {Holík} and Ondřej {Lengál} and Yu-Fang {Chen}",
  title="Z3-Noodler: An Automata-based String Solver",
  booktitle="Proceedings of TACAS'24",
  year="2024",
  series="Lecture Notes",
  journal="Lecture Notes in Computer Science",
  number="14570",
  pages="24--33",
  publisher="Springer Verlag",
  address="Luxembourgh",
  doi="10.1007/978-3-031-57246-3\{_}2",
  issn="0302-9743",
  url="https://link.springer.com/chapter/10.1007/978-3-031-57246-3_2"
}