Publication Details

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

CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; HRANIČKA, J.; LENGÁL, O.; SÍČ, J. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. Proceedings of TACAS'25. Lecture Notes in Computer Science. Hamilton: Springer Verlag, 2025. 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)
Havlena Vojtěch, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Hranička Jan, Bc.
Lengál Ondřej, Ing., Ph.D. (DITS)
Síč Juraj, Mgr. (DITS)
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
BibTeX 
@inproceedings{BUT194210,
  author="David {Chocholatý} and Vojtěch {Havlena} and Lukáš {Holík} and Jan {Hranička} and Ondřej {Lengál} and Juraj {Síč}",
  title="Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation",
  booktitle="Proceedings of TACAS'25",
  year="2025",
  journal="Lecture Notes in Computer Science",
  pages="22",
  publisher="Springer Verlag",
  address="Hamilton",
  issn="0302-9743"
}
Back to top