Software Model Checking: The VeriSoft Approach

Verification by state-space exploration, also often referred to as {em model checking}, is an effective method for analyzing the correctness of concurrent reactive systems (for instance, communication protocols). Unfortunately, traditional model checking is restricted to the verification of properties of models, i.e., {em abstractions}, of concurrent systems. We discuss in this paper how model checking can be extended to analyze arbitrary {em software}, such as implementations of communication protocols written in programming languages like C or C++. We then introduce a search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in {em VeriSoft}, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code. During the past five years, VeriSoft has been applied successfully for analyzing several software products developed in Lucent Technologies, and has also been licensed to hundreds of users in industry and academia. We discuss applications, strengths and limitations of VeriSoft, and compare it to other approaches to software model checking, analysis and testing.