Detail publikačního výsledku

Z3-Noodler: An Automata-based String Solver

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

Originální název

Z3-Noodler: An Automata-based String Solver

Anglický název

Z3-Noodler: An Automata-based String Solver

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows that Z3-Noodler is a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.

Anglický abstrakt

Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows that Z3-Noodler is a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.

Klíčová slova

String solving, finite automata, SMT solving

Klíčová slova v angličtině

String solving, finite automata, SMT solving

Autoři

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

Rok RIV

2025

Vydáno

04.04.2024

Nakladatel

Springer Verlag

Místo

Luxembourgh

Kniha

Proceedings of TACAS'24

Periodikum

Lecture Notes in Computer Science

Číslo

14570

Stát

Švýcarská konfederace

Strany od

24

Strany do

33

Strany počet

10

URL

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

Plný text v Digitální knihovně

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

BibTex

@inproceedings{BUT188550,
  author="Yu-Fang {Chen} and David {Chocholatý} and Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Juraj {Síč}",
  title="Z3-Noodler: An Automata-based String Solver",
  booktitle="Proceedings of TACAS'24",
  year="2024",
  journal="Lecture Notes in Computer Science",
  number="14570",
  pages="24--33",
  publisher="Springer Verlag",
  address="Luxembourgh",
  doi="10.1007/978-3-031-57246-3\{_}2",
  url="https://link.springer.com/chapter/10.1007/978-3-031-57246-3_2"
}