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

Autoři:Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš
Typ:software
Vznik:2018
Licence:vyžadována - zdarma
Klíčová slova:Alternating Finite Automata, Decision Procedure, IC3, String Solving
Popis:
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.
Umístění:
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
Výzkumné skupiny:
Pracoviště:
Licenční podmínky:
Free software under the terms of GNU GPLv3 (cf.http://www.gnu.org/licenses/gpl.html).

Vaše IPv4 adresa: 54.234.227.202
Přepnout na https