Detail publikace

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

Typ

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

Jazyk

angličtina

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.

Klíčová slova

String solving, finite automata, SMT solving

Autoři

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

Vydáno

4. 4. 2024

Nakladatel

Springer Verlag

Místo

Luxembourgh

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

14570

Stát

Spolková republika Německo

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",
  series="Lecture Notes",
  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",
  issn="0302-9743",
  url="https://link.springer.com/chapter/10.1007/978-3-031-57246-3_2"
}