Verifying safety properties of concurrent Java programs using 3-valued logic

Abstract We provide a parametric framework for verifying safety properties of concurrent Java programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to error-detection algorithms that are more precise than existing techniques. The framework also provides the most precise shape-analysis algorithm for concurrent programs. In contrast to existing verification techniques, we do not put a bound on the number of allocated objects. The framework even produces interesting results when analyzing Java programs with an unbounded number of threads. The framework is applied to successfully verify the following properties of a concurrent program: ffl Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant [18]. ffl The program does not perform inconsistent updates due to interference. ffl The program does not reach a deadlock. ffl The program does not produce run-time errors due to illegal thread interactions. We also find bugs in erroneous versions of such implementations. A prototype of our framework has been implemented. 1 Introduction Java provides low-level concurrency-control constructs that enable the programmer to create complicated and powerful synchronization schemes. The Java language provides no means of compile-time or run-time checking for the correctness of concurrent behavior. This makes concurrent programming in Java quite error-prone (e.g., [38])