Inductive Proof Outlines for Monitors in Java

The research concerning Java’s semantics and proof theory has mainly focussed on various aspects of sequential sub-languages. Java, however, integrates features of a class-based object-oriented language with the notion of multi-threading, where multiple threads can concurrently execute and exchange information via shared instance variables. Furthermore, each object can act as a monitor to assure mutual exclusion or to coordinate between threads. In this paper we present a sound and relatively complete assertional proof system for Java’s monitor concept, which generates verification conditions for a concurrent sublanguage JavaMT of Java. This work extends previous results by incorporating Java’s monitor methods.

• Type: Conference
• Year: 2003
• Where: FMOODS
• Authors: Erika Ábrahám, Frank S. de Boer, Willem P. de Roever, Martin Steffen
• Keywords: FMOODS 2003, FMOODS 2007, Java’s Monitor, Java’s Monitor Concept, Research Concerning Java