Sciweavers

Share
FMOODS
2003

Inductive Proof Outlines for Monitors in Java

9 years 12 months ago
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.
Erika Ábrahám, Frank S. de Boer, Wil
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where FMOODS
Authors Erika Ábrahám, Frank S. de Boer, Willem P. de Roever, Martin Steffen
Comments (0)
books