Sloth: An SMT Solver for String Constraints

Lenochod - SMT solver pro řetězcová omezení

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

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

Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Janků Petr, Ing. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Lin Anthony (FIT)
Rummer Philipp

Alternating Finite Automata, Decision Procedure, IC3, String Solving

Lenochod je rozhodovaci procedura pro několik fragmentů řetězcových omezení, zahrnující tzv. straight-line fragment a acyklicke formule. Narozdil od většiny řetězcových solverů je Sloth schopný rozhodnout splnitelnost omezení kombinující konkatenaci, regulární výrazy a převodníky. Sloth používá stručné alternující konečné automaty (AKA) jako stručné symbolické reprezentace řetězcových omezení a používá moderní algoritmy pro ověření modelů jako IC3 pro řešení prázdnosti AKA.

Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/sloth/ (http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/) a https://github.com/uuverifiers/sloth

AQUAS: Agregované metody řízení kvality, EU, Horizon 2020, 8A17001, 737475, 2017-2020, ukončen
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, ukončen
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, 2016-2018, řešení
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, 2017-2019, řešení

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

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