DECO is a static DEadlock analyzer for concurrent objects. It analyzes programs written in ABS and returns a description of possible deadlocks that might occur in runtime. The tool performs a sound analysis, that is, if no deadlocks are found, the analyzed program is guaranteed to be deadlock free.
DECO is based on a object-sensitive points-to analysis combined with a precise May-Happen-in-Parallel analysis. With the result of the points-to analysis, DECO builds a dependency graph. Any cycle in such graph represents a possible deadlock. The MHP analysis is then applied to discard unfeasible cycles.