Technical Report TR536:
Model-Checking Multi-Threaded Distributed Java Programs
Scott D. Stoller
(Jan 2000), 25 pages pages
[Revised May 2000 and September 2000.]
- Abstract:
-
Systematic state-space exploration is a powerful technique for verification of concurrent software systems. Most work in this area deals with manually-constructed models of those systems. We propose a framework for applying state-space exploration to multi-threaded distributed systems written in standard programming languages. It generalizes Godefroid's work on VeriSoft, which does not handle multi-threaded systems, and Bruening's work on ExitBlockRW, which does not handle distributed (multiprocess) systems. Unlike ExitBlockRW, our search algorithms incorporate powerful partial-order methods, guarantee detection of deadlocks, and guarantee detection of violations of the locking discipline used to avoid race conditions in accesses to shared variables.
- Available as:
-
