Detail produktu
Sloth: An SMT Solver for String Constraints
Vznik: 2018
Janků Petr, Ing., Ph.D. (VZ VERIFIT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Lin Anthony
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
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, zahájení: 2016-01-01, ukončení: 2018-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen