A practical presentation of JaDA is given, highlighting the main connections between the tool and the theory behind it and presenting some of the features for customising the analysis.
JaDA is a static deadlock analyzer that targets Java bytecode. The core of JaDA is a behavioral type system especially designed to record dependencies between concurrent code. These behavioral types are thereafter analyzed by means of a fixpoint algorithm that reports potential deadlocks in the original Java code. We give a practical presentation of JaDA , highlighting the main connections between the tool and the theory behind it and presenting some of the features for customising the analysis. We finally assess JaDA against the current state-of-the-art tools, including a commercial grade one.