PICoSo: An SMT Solver for String Constraints

Název česky

PICoSo: SMT řešič pro řezězcová omezení

Typ

software

Licence

vyžadována - zdarma

Autoři

Holíková Lenka, Ing. (UITS FIT VUT)
Janků Petr, Ing. (UITS FIT VUT)

Popis

PICoSo obsahuje rozšířenou rozhodovací proceduru pro tzv. straight-line fragment. Narozdil od nástroje Sloth je PICoSo je schopný řešit omezení kombinující konkatenaci, regulární výrazy, převodníky a délková omezení. PICoSo používá vylepšenou verzi Parikh image abstrakce konečných automatů pro vyřešení omezení délky řetězce.

Umístění

Nástroj a dodatečné informace se nacházejí na ...

Licence

Free software under the terms of GNU GPLv3 (cf.http://www.gnu.org/licenses/gpl.html).

Projekty

Bezpečné a spolehlivé počítačové systémy (FIT-S-17-4014)
IT4Innovations excellence in science (LQ1602)
Pokročilé metody hluboké inspekce v aplikační vrstvě pro obranu proti dnešním hrozbám (FEKT/FIT-J-19-5906)
ROBUST - Verifikace a hledání chyb v pokročilém softwaru (GA17-12465S)

Výzkumné skupiny

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

Pracoviště

Ústav inteligentních systémů FIT VUT v Brně (UITS FIT VUT)