JaDA – the Java Deadlock Analyzer

JaDA is a static deadlock analyzer that targets Java byte-code. The core of JaDA is a behavioral type system especially designed to record dependencies between concurrent code. These behavioural 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. We also present some of the features for cus-tomising the analysis: while the main strength of JaDA is to run in a fully automatic way, user interaction is however possible and may enhance the accuracy of the results. We finally assess JaDA against the current state-of-the-art tools, including a commercial grade one. As one of the main achievements so far, we present the successful analysis of a recursive method that creates a potentially infinite number of threads.