Sloth: An SMT Solver for String Constraints

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

software

vyžadována - zdarma

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

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/ a https://github.com/uuverifiers/sloth

AQUAS: Agregované metody řízení kvality (8A17001)
Bezpečné a spolehlivé počítačové systémy (FIT-S-17-4014)
Efektivní automaty pro formální rozhodování (GJ16-24707Y)
IT4Innovations excellence in science (LQ1602)
ROBUST - Verifikace a hledání chyb v pokročilém softwaru (GA17-12465S)

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

University of Oxford (UOx)
Uppsala University (Uppsala)
Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)