Detail výsledku

Z3-Noodler: An Automata-based String Solver

CHEN, Y.; CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Z3-Noodler: An Automata-based String Solver. Proceedings of TACAS'24. Lecture Notes in Computer Science. Lecture Notes. Luxembourgh: Springer Verlag, 2024. no. 14570, p. 24-33. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Chen Yu-Fang
Chocholatý David, Ing., UITS (FIT)
Havlena Vojtěch, Ing., Ph.D., UITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Síč Juraj, Mgr., UITS (FIT)
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

URL
Rok
2024
Strany
24–33
Časopis
Lecture Notes in Computer Science, č. 14570, ISSN 0302-9743
Sborník
Proceedings of TACAS'24
Řada
Lecture Notes
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'24 (TACAS'24)
Vydavatel
Springer Verlag
Místo
Luxembourgh
DOI
10.1007/978-3-031-57246-3_2
UT WoS
001284177100002
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"
}
Soubory
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury, GAČR, Standardní projekty, GA23-07565S, zahájení: 2023-01-01, ukončení: 2025-12-31, řešení
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru