Sciweavers

Share
FUIN
2008

A Deductive Proof System for Multithreaded Java with Exceptions

8 years 10 months ago
A Deductive Proof System for Multithreaded Java with Exceptions
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. Besides that, the language offers a flexible exception mechanism for handling errors or exceptional program conditions. To reason about safety-properties of Java-programs and extending previous work on the proof theory for monitor synchronization, we introduce in this paper an assertional proof method for JavaMT ("Multi-Threaded Java"), a small concurrent sublanguage of Java, covering concurrency and especially exception handling. We show soundness and relative completeness of the proof method.
Erika Ábrahám, Frank S. de Boer, Wil
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FUIN
Authors Erika Ábrahám, Frank S. de Boer, Willem P. de Roever, Martin Steffen
Comments (0)
books