Publication Details

Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation

CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, HRANIČKA Jan, LENGÁL Ondřej and SÍČ Juraj. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In: Proceedings of TACAS'25. Hamilton: Springer Verlag, 2025, p. 22. ISSN 0302-9743.
Czech title
Z3-Noodler 1.3: Navádění rozhodovacích procedur pro řetězce s generováním modelu
Type
conference paper
Language
english
Authors
Chocholatý David, Ing. (DITS FIT BUT)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Hranička Jan, Bc. (FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
Keywords

SMT, string constraints, noodlification, automata, SMT solver

Abstract

Z3-Noodler is a fork of the Z3 SMT solver replacing its string theory implementation with a portfolio of decision procedures and a selection mechanism for choosing among them based on the features of the input formula. In this paper, we give an overview of the used decision procedures, including a novel length-based procedure, and their integration into a robust solver with a good overall performance, as witnessed by Z3-Noodler winning the string division of SMT-COMP'24 by a large margin. We also extended the solver with a support for model generation, which is essential for the use of the solver in practice.

Published
2025 (in print)
Pages
22
Journal
Lecture Notes in Computer Science, ISSN 0302-9743
Proceedings
Proceedings of TACAS'25
Conference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25, Hamilton, CA
Publisher
Springer Verlag
Place
Hamilton, CA
BibTeX 
@INPROCEEDINGS{FITPUB13351,
   author = "David Chocholat\'{y} and Vojt\v{e}ch Havlena and Luk\'{a}\v{s} Hol\'{i}k and Jan Hrani\v{c}ka and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c}",
   title = "Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation",
   pages = 22,
   booktitle = "Proceedings of TACAS'25",
   journal = "Lecture Notes in Computer Science",
   year = 2025,
   location = "Hamilton, CA",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13351"
}
Back to top