JaDA -- the Java Deadlock Analyzer

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.