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.

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: Scott D. Stoller
• Keywords: Guarantee Detection, Multi-threaded Distributed Systems, SPIN 2000, State-space Exploration, Theoretical Computer Science