Deadlock detection of Java Bytecode

TL;DR

This paper introduces a novel deadlock detection technique for Java bytecode that leverages typing rules to create abstract models of dependencies and employs an extended solver for deadlock analysis, supported by a prototype verifier.

Contribution

It presents a new method for deadlock detection in Java bytecode using abstract models and an extended solver, covering most Java features.

Findings

Effective deadlock detection in Java bytecode

Prototype verifier covers most Java features

Models enable analysis of infinite-state dependencies

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.