Z3-Noodler: A String Solver

Název česky

Z3-Noodler: Řetězcový Řešič

Typ

software

Licence

Využití výsledku jiným subjektem je možné bez nabytí licence (výsledek není licencován)

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Autoři

Havlena Vojtěch, Ing., Ph.D. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Chocholatý David, Ing. (UITS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Síč Juraj, Mgr. (UITS)
Chen Yu-Fang

Klíčová slova

string solving noodlification automata

Popis

Z3-Noodler je fork SMT řešiče Z3, který nahrazuje jeho řešič teorie řetězců vlastním řešičem implementujícím nedávno zavedený algoritmus založený na stabilizaci pro řešení slovních rovnic s regulárními omezeními.

Umístění

https://github.com/VeriFIT/z3-noodler

Licenční podmínky

Volně šiřitelný software pod MIT licencí https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE

Projekty

Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, 2020-2024, řešení
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, 2023-2026, řešení
Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury, GAČR, Standardní projekty, GA23-07565S, 2023-2025, řešení

Výzkumné skupiny

Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)

Pracoviště

Ústav inteligentních systémů (UITS)