This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.
Deadlock detection of java bytecode / Laneve, Cosimo*; Garcia, Abel. - ELETTRONICO. - 10855:(2018), pp. 37-53. (Intervento presentato al convegno 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017 tenutosi a bel nel 2017) [10.1007/978-3-319-94460-9_3].
Deadlock detection of java bytecode
Laneve, Cosimo
;Garcia, Abel
2018
Abstract
This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
