Verifying Safety Properties of Concurrent Java Programs Using
3-Valued Logic
  
Abstract:
 
We provide a parametric framework for verifying 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.
   
This work is part of Ph.D. of Eran Yahav
(http://www.cs.tau.ac.il/~yahave).

A prototype of the framework has been implemented using TVLA 
(http://www.math.tau.ac.il/~rumster/TVLA).