Verification for Java's monitor concept
Speaker: Willem-Paul de Roever, University of Kiel
When: 2006-10-05 10:00:00
Venue: 78-420
Host: Ian Hayes
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
maessage 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.
Biography:(biography unavailable)
Type: SSE Seminar
Contact:Ian Hayes, seminar host ()
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)