Detail produktu

Sloth: An SMT Solver for String Constraints

Vznik: 2018

Název česky
Lenochod - SMT solver pro řetězcová omezení
Typ
software
Licence
vyžadována - zdarma
Autoři
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)
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í
Projekty
Výzkumné skupiny
Pracoviště
Nahoru