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:
1. Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant
\cite{kn:Hoare75}.
2. The program does not perform inconsistent updates due to interference.
3. 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.