Using shape analysis to reduce finite-state models of concurrent Java programs

Abstract

Finite-state verification (e.g., model checking) provides a powerful means to detect concurrency errors, which are often subtle and difficult to reproduce. Nevertheless, widespread use of this technology by developers is unlikely until tools provide automated support for extracting the required finite-state models directly from program source. Unfortunately, the dynamic features of modern languages such as Java complicate the construction of compact finite-state models for verification. In this article, we show how shape analysis, which has traditionally been used for computing alias information in optimizers, can be used to greatly reduce the size of finite-state models of concurrent Java programs by determining which heap-allocated variables are accessible only by a single thread, and which shared variables are protected by locks We also provide several other state-space reductions based on the semantics of Java monitors. A prototype implementation of the reductions demonstrates their effectiveness. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Veriflcation General Terms: Verification.