Verification of Multithreaded Object-Oriented Programs with Invariants

Abstract

Developing safe multithreaded software systems is difficult due to the potential unwanted interference among concurrent threads. This paper presents a sound, modular, and simple verification tech-nique for multithreaded object-oriented programs with object in-variants. Based on a recent methodology for object invariants in single-threaded programs, this new verification technique enables leak-proof ownership domains. These domains guarantee that only one thread at a time can access a confined object. A primary aim of a reliable software system is ensuring that all objects in the system maintain consistent states: states in which all fields, and all fields of other objects on which they depend, contain legal meaningful values. In this paper, we formalize consistency