PICoSo: An SMT Solver for String Constraints

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

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

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

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

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.

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

Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, completed
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, completed
Pokročilé metody hluboké inspekce v aplikační vrstvě pro obranu proti dnešním hrozbám, BUT, Vnitřní projekty VUT, FEKT/FIT-J-19-5906, 2019-2020, completed
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware, GACR, Standardní projekty, GA17-12465S, 2017-2019, running

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)