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., FIT (FIT)
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

https://link.springer.com/chapter/10.1007/978-3-031-90653-4_2

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

pdf 978-3-031-90653-4_2.pdf 2 MB

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

Automata@FIT (RG Automata@FIT)
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)