Publication result detail

Z3-Noodler: An Automata-based String Solver

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

Original Title

Z3-Noodler: An Automata-based String Solver

English Title

Z3-Noodler: An Automata-based String Solver

Type

Paper in proceedings outside WoS and Scopus

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.

English 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

Key words in English

String solving, finite automata, SMT solving

Authors

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

RIV year

2025

Released

04.04.2024

Publisher

Springer Verlag

Location

Luxembourgh

Book

Proceedings of TACAS'24

Edition

Lecture Notes

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

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"
}

Documents

978-3-031-57246-3_2