Publication Details

Z3-Noodler: An Automata-based String Solver

HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Z3-Noodler: An Automata-based String Solver. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, pp. 24-33. ISSN 0302-9743. Available from: https://link.springer.com/chapter/10.1007/978-3-031-57246-3_2
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 FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Chocholatý David, Bc. (FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
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
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, LU
DOI
10.1007/978-3-031-57246-3_2
BibTeX 
@INPROCEEDINGS{FITPUB13193,
   author = "Vojt\v{e}ch Havlena and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and David Chocholat\'{y} and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c}",
   title = "Z3-Noodler: An Automata-based String Solver",
   pages = "24--33",
   booktitle = "Proceedings of TACAS'24",
   journal = "Lecture Notes in Computer Science",
   number = 14570,
   year = 2024,
   location = "Luxembourgh, LU",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-031-57246-3\_2",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13193"
}
Back to top