Detail publikačního 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.

Originální název

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

Anglický název

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

Druh

Stať ve sborníku mimo WoS a Scopus

Originální 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.

Anglický 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

Klíčová slova v angličtině

SMT, string constraints, noodlification, automata, SMT solver

Autoři

CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; HRANIČKA, J.; LENGÁL, O.; SÍČ, J.

Rok RIV

2026

Vydáno

03.05.2025

Nakladatel

Springer Verlag

Místo

Hamilton

Kniha

Proceedings of TACAS'25

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

15697

Číslo

1

Stát

Spolková republika Německo

Strany od

23

Strany do

44

Strany počet

22

URL

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

Plný text v Digitální knihovně

http://hdl.handle.net/11012/255206

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"
}