Publication detail

Z3-Noodler: An Automata-based String Solver

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

Original Title

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

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

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

Pages to

Pages count

URL

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

Full text in the Digital Library

http://hdl.handle.net/11012/252870

BibTex

@inproceedings{BUT188550,
  author="Yu-Fang {Chen} and David {Chocholatý} and Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Juraj {Síč}",
  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"
}