Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Chocholatý David, Ing., UITS (FIT)
Havlena Vojtěch, Ing., Ph.D., UITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Hranička Jan, Bc., FIT (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Síč Juraj, Mgr., UITS (FIT)
Abstrakt

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.

Klíčová slova

SMT, string constraints, noodlification, automata, SMT solver

URL
Rok
2025
Strany
23–44
Časopis
Lecture Notes in Computer Science, roč. 15697, č. 1, ISSN 0302-9743
Sborník
Proceedings of TACAS'25
Konference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25
Vydavatel
Springer Verlag
Místo
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"
}
Soubory
Projekty
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury, GAČR, Standardní projekty, GA23-07565S, zahájení: 2023-01-01, ukončení: 2025-12-31, řešení
Verification and Analysis for Safety and Security of Applications in Life, EU, HORIZON EUROPE, SEP-210979090, zahájení: 2024-06-01, ukončení: 2027-05-31, řešení
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru