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.
Abel Garcia, Cosimo Laneve (2017). JaDA - A Static Java Deadlock Analizer.
JaDA - A Static Java Deadlock Analizer
Abel Garcia;Cosimo Laneve
2017
Abstract
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.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
