Model-checking multi-threaded distributed Java programs

Abstract. Systematic state-space exploration is a powerful technique for verication 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 dis-tributed systems written in standard programming languages. It general-izes 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 al-gorithms incorporate powerful partial-order methods, guarantee detec-tion of deadlocks, and guarantee detection of violations of the locking discipline used to avoid race conditions in accesses to shared variables.