Publication Details

Z3-Noodler: An Automata-based String Solver

HAVLENA, V.; CHOCHOLATÝ, D.; SÍČ, J.; HOLÍK, L.; LENGÁL, O.; CHEN, Y. Z3-Noodler: An Automata-based String Solver. Proceedings of TACAS'24. Lecture Notes in Computer Science. Lecture Notes. Luxembourgh: Springer Verlag, 2024. p. 24-33. ISSN: 0302-9743.
Czech title
Z3-Noodler: Řetězcový řešič založený na automatech
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS)
Chocholatý David, Ing. (DITS)
Síč Juraj, Mgr. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Chen Yu-Fang
URL
Keywords

String solving, finite automata, SMT solving

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.

Published
2024
Pages
24–33
Journal
Lecture Notes in Computer Science, no. 14570, ISSN 0302-9743
Proceedings
Proceedings of TACAS'24
Series
Lecture Notes
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'24 (TACAS'24), Centre for Security, Reliability and Trust (SnT), University of Luxembourg., LU
Publisher
Springer Verlag
Place
Luxembourgh
DOI
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"
}
Back to top