Product Details

PICoSo: An SMT Solver for String Constraints

Created: 2019

Czech title
PICoSo: SMT řešič pro řezězcová omezení
Type
software
License
required - free
Authors
Holíková Lenka, Ing. (DITS FIT BUT)
Janků Petr, Ing. (DITS FIT BUT)
Keywords

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

Description

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.

Projects
Research groups
Departments
Back to top