PICASSO: a PI-CAlculus-based Static SOftware analyzer. Picasso is a static analyzer for depth-bounded systems (DBS). The main use case of Picasso is to take a DBS [as input] and compute an over-approximations of its covering set. DBS are well-structured graph rewriting systems that generalize Petri nets and subsume a diverse range of infinite-state systems. Picasso computes an invariant of the input DBS by using specialized algorithms that exploit the monotonic structure of DBS.