Software Model Checking: The VeriSoft Approach
01 January 2005
We discuss in this paper how model checking can be extended to analyze arbitrary 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 VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code.