Applied result detail

PICoSo: An SMT Solver for String Constraints

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

Original Title

PICoSo: An SMT Solver for String Constraints

English Title

PICoSo: An SMT Solver for String Constraints

Type

Software

Abstract

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.

Abstract in English

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.

Keywords

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

Key words in English

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

Location

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

Licence fee

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

www

https://www.fit.vut.cz/research/product/620/