Details

Autor(en) / Beteiligte

• Yahav, Eran

Titel

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

Ist Teil von

• Annual Symposium on Principles of Programming Languages: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages : London, United Kingdom, 2001, p.27-40

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

2001

Link zum Volltext

Quelle

ACM Digital Library

Beschreibungen/Notizen

• 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: *Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant [19]. *The program does not perform inconsistent updates due to interference. *The program does not reach a deadlock. *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.