Result 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. no. 1, p. 23-44. ISSN: 0302-9743.
Type
conference paper
Language
English
Authors
Chocholatý David, Ing., DITS (FIT)
Havlena Vojtěch, Ing., Ph.D., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Hranička Jan, Bc.
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Síč Juraj, Mgr., DITS (FIT)
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.

Keywords

SMT, string constraints, noodlification, automata, SMT solver

URL
Published
2025
Pages
23–44
Journal
Lecture Notes in Computer Science, vol. 15697, no. 1, 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
Publisher
Springer Verlag
Place
Hamilton
DOI
10.1007/978-3-031-90653-4_2
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",
  volume="15697",
  number="1",
  pages="23--44",
  publisher="Springer Verlag",
  address="Hamilton",
  doi="10.1007/978-3-031-90653-4\{_}2",
  issn="0302-9743",
  url="https://link.springer.com/chapter/10.1007/978-3-031-90653-4_2"
}
Files
Projects
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, start: 2023-01-01, end: 2025-12-31, running
Verification and Analysis for Safety and Security of Applications in Life, EU, HORIZON EUROPE, SEP-210979090, start: 2024-06-01, end: 2027-05-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top