PICoSo: An SMT Solver for String Constraints

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

software

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Poskytovatel licence na výsledek nepožaduje licenční poplatek

Holíková Lenka, Ing., Ph.D. (UITS)
Janků Petr, Ing. (UITS)

String constraint solving, Program verification, Parikh Image, Alternating Finite Automata, Decision Procedure

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.

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

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

Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, ukončen
Pokročilé metody hluboké inspekce v aplikační vrstvě pro obranu proti dnešním hrozbám, VUT, Vnitřní projekty VUT, FEKT/FIT-J-19-5906, 2019-2020, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, 2017-2019, řešení

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

Ústav inteligentních systémů (UITS)