Detail aplikovaného výsledku

PICoSo: An SMT Solver for String Constraints

HOLÍKOVÁ, L.; JANKŮ, P.

Originální název

PICoSo: An SMT Solver for String Constraints

Anglický název

PICoSo: An SMT Solver for String Constraints

Druh

Software

Abstrakt

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.

Abstrakt aglicky

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

Klíčová slova anglicky

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 ...

Licenční poplatek

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

www