An Assertional Proof System for Multithreaded Java - Theory and Tool Support

Leiden Repository

An Assertional Proof System for Multithreaded Java - Theory and Tool Support

Type: Doctoral Thesis
Title: An Assertional Proof System for Multithreaded Java - Theory and Tool Support
Author: Abraham, E.
Publisher: Leiden University, Faculty of Mathematics & Natural Sciences, Institute for Programming research and Algorithmics
Issue Date: 2005-01-20
Keywords: Java programming language
Multithreading
Monitors
Verification
Hoare-logic
Abstract: Besides 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 shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about safety properties of multithreaded Java programs, we introduce a tool-supported assertional proof method for JavaMT ("Multi-Threaded Java"), a small 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 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.
Description: Promotores: J.N. Kok, W.-P. de Roever. Co-promotores: F.S. de Boer, M. Steffen.
With summary in Dutch
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Abraham, E., 2005. Doctoral thesis, Leiden University
Series/Report no.: IPA Dissertation Series;2005-01
ISBN: 9090189084
Sponsor: IST project Omega (IST-2001-33522) NWO/DFG project Mobi-J (RO 1122/9-1, RO 1122/9-2)
Handle: http://hdl.handle.net/1887/584
 

Files in this item

Description Size View
application/postscript Full text (ps file) 30.45Mb View/Open
application/pdf Full text 21.18Mb View/Open

This item appears in the following Collection(s)