Detail publikace

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

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.

Klíčová slova

SMT, string constraints, noodlification, automata, SMT solver

Autoři

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

Vydáno

3. 5. 2025

Nakladatel

Springer Verlag

Místo

Hamilton

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

15697

Stát

Spolková republika Německo

Strany od

Strany do

Strany počet

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",
  number="15697",
  pages="23--44",
  publisher="Springer Verlag",
  address="Hamilton",
  doi="10.1007/978-3-031-90653-4\{_}2",
  issn="0302-9743"
}