Verification for Java's multi-threading and monitor concepts

Abstract

Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation.

To reason about safety properties of multithreaded Java programs, we introduce an assertional proof method for a multithreaded sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java.

The verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behaviour of a single instance, and global ones taking care of the connections between objects. From the annotated program, a translator tool generates a number of verification conditions which are handled over to the interactive theorem prover PVS.