Verification for Java’s reentrant multithreading concept. (English) Zbl 1077.68552

Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 5-20 (2002).
Summary: 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 offers coordination via lock-synchronization, and communication by synchronous message passing, including re-entrant method calls, and by instance variables shared among threads.
To reason about multithreaded programs, we introduce in this paper an assertional proof method for Java\(_{\text{MT}}\) (“Multi-Threaded Java”), a small concurrent sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java, i.e., object creation, side effects, and aliasing, but leaving aside inheritance and subtyping.
For the entire collection see [Zbl 0989.00051].


68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Full Text: Link