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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Zufferey, Damien; Wies, Thomas; Henzinger, Thomas A.: Ideal abstractions for well-structured transition systems (2012)