"Model-Checking" Software with VeriSoft

Abstract

VeriSoft is a tool for systematically exploring the state spaces of software systems composed of several concurrent processes executing arbitrary code written in full-fledged programming languages, such as C or C++. The state space of a system is a directed graph that represents the combined behavior of all the components of the system. VeriSoft explores the state space of a system by controlling and observing the execution of all the components, and by reinitializing their executions. It searches for coordination problems (deadlocks, divergences, etc.) between concurrent components, and for violations of user-specified assertions. VeriSoft can always guarantee a complete coverage of the state space up to some depth. It also supports a special operation to simulate nondeterminism. This operation can be used anywhere (any language, any process) to easily model the environment of an open system.

VeriSoft has been applied successfully for analyzing (testing, debugging, reverse-engineering) several software products developed in Lucent Technologies, such as telephone-switching applications. Since VeriSoft can automatically generate, execute and evaluate thousands of tests per minute and has complete control over nondeterminism, it can quickly reveal behaviors that are virtually impossible to detect using conventional testing techniques.

In this talk, I will present VeriSoft, what it does, how it works (search algorithms), industrial applications, and discuss related work and future work.