Verification for Java's monitor concept

Speaker: Willem-Paul de Roever (University of Kiel)

When: 10:00, Thursday, 5 October 2006

Venue: 78-420

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.

Hospitality: Ian Hayes

Contact: Phil Cook (SSE seminar co-ordinator) (philc@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html