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.
This site is still under construction. Therefore, there are still many gaps to fill (the manual!!). We will fill them as time permits.
A DBS is a graph rewriting system for which there exists a bound on the length of all acyclic paths in all reachable graphs of the system.
Often, the graph rewriting models of concurrent programs are depth-bounded or have natural depth-bounded abstractions that preserve important properties such as safety and progress guarantees.
DBS are also well-structured transition systems (WSTS), which makes them amenable to automated analysis.
A WSTS is a transition system equipped with a well-quasi-ordering that is monotonic with respect to state transitions, i.e., states that are small in the ordering exhibit less behavior than larger states.
Many verification problems of a WSTS can be reduced to computing its covering set, which is the downward closure (with respect to the ordering) of the set of all reachable states of the system.
In the case of DBS the ordering used is subgraph isomorphism.
A graph G1 is smaller than G2 if it is a subgraph of G2.
Input formats. Picasso has two main frontends: a graph rewriting frontend presented and a simple high-level language inspired by early actor-model languages. In fact, this language just provides a convenient syntax for sets of recursive equations in the π -calculus. The programs written in the actor language are compiled into a graph rewriting system and then analyzed as such. The grammars of the input formats is in the manual.
Analyses and outputs. The default analysis of Picasso is to compute the covering set of a given DBS. Picasso produces an HTML report that contains the textual input and a graphical representation of the rewrite rules, the graphs representing the initial states and the computed covering set. If the input system is expressed in terms of the actor language, then the control-flow automaton of each actor is also included in the report.