Skip to Main content Skip to Navigation
Book sections

JaDA – the Java Deadlock Analyzer

Abel Garcia 1, 2 Cosimo Laneve 2, 1
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : 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.
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download
Contributor : Laneve Cosimo <>
Submitted on : Wednesday, December 6, 2017 - 11:39:39 AM
Last modification on : Friday, October 30, 2020 - 12:04:03 PM


Files produced by the author(s)


  • HAL Id : hal-01643216, version 1



Abel Garcia, Cosimo Laneve. JaDA – the Java Deadlock Analyzer. Simon Gay; Antonio Ravara. Behavioural Types: from Theory to Tools, River Publishers, pp.169-192, 2017. ⟨hal-01643216⟩



Record views


Files downloads