PICoSo: An SMT Solver for String Constraints

Typ

software

Jazyk

anglicky

Autoři

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

Popis

PICoSo contains an extended decision procedure for the straight-line fragment. In contrast to Sloth, PICoSo is able to solve constraints combining concatenation, regular expressions, transduction and length constraints. PICoSo uses a refined version of the Parikh image abstraction of finite automata to resolve string length constraints.

Klíčová slova

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

Umístění

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

Licence

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

Licenční poplatek

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

Licenční podmínky

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, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, 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
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, zahájení: 2019-03-01, ukončení: 2020-02-28, 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

Výzkumné skupiny

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

Pracoviště

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