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.
2017
Abel Garcia, Cosimo Laneve (2017). JaDA - A Static Java Deadlock Analizer.
Abel Garcia; Cosimo Laneve
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/669720
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact