Model-Checking Multi-threaded Distributed Java Programs

11 years 11 months ago
Model-Checking Multi-threaded Distributed Java Programs
Systematic state-space exploration is a powerful technique for veri cation 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 multi-process 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.
Scott D. Stoller
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SPIN
Authors Scott D. Stoller
Comments (0)