A static (Ja)va (D)eadlock (A)nalyzer
JaDAanalyzes deadlock presences in Java programs by analyzing the behaviors of the Java bytecode
JaDA detects deadlocks of Java programs at static time.
The tool uses typing rules to extract infinite-state abstract models of the dependencies among
the diferent components of the Java intermediate language
JVML, the Java bytecode.
These models are subsequently analyzed by means of a fixpoint decision algorithm that
we have defined for detecting deadlocks in process calculi. JaDA also exhibits the executions
causing deadlocks and allows users to analyze false positives.
This prototype covers most of the Java language features.
Browse our site to know more details about the Static Resource Analysis research.