PICoSo: An SMT Solver for String Constraints

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.