An assertion-based proof system for multithreaded Java

AbstractBesides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes synchronous message passing, dynamic thread creation, shared-variable concurrency via instance variables, and coordination via reentrant synchronization monitors.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 behavior of a single instance, and global ones taking care of the connections between objects. We establish the soundness and the relative completeness of the proof system. From an annotated program, a number of verification conditions are generated and handed over to the interactive theorem prover PVS