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 (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.
CITATION STYLE
Stoller, S. D. (2000). Model-checking multi-threaded distributed Java programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1885, pp. 224–244). Springer Verlag. https://doi.org/10.1007/10722468_14
Mendeley helps you to discover research relevant for your work.