This paper discusses the extension of model checking to directly analyze "actual" descriptions of concurrent systems, such as implementations of communication protocols written in programming languages like C or C++. The authors introduce a new search technique suitable for exploring the state spaces of such systems, which has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of concurrent processes executing arbitrary C code. The paper highlights the limitations of existing state-space exploration techniques, which are restricted to analyzing systems where each state can be uniquely identified. The proposed search algorithm does not rely on this assumption, making it applicable to systems with complex state representations. The effectiveness of the new technique is demonstrated through an example where VeriSoft successfully discovered an error in a 2500-line C program controlling robots in an unpredictable environment. The paper also provides a detailed explanation of the concurrent system model, the dynamic semantics, and the state-space exploration techniques used, including the use of persistent sets and sleep sets to improve efficiency and reduce the risk of incompleteness in verification results.This paper discusses the extension of model checking to directly analyze "actual" descriptions of concurrent systems, such as implementations of communication protocols written in programming languages like C or C++. The authors introduce a new search technique suitable for exploring the state spaces of such systems, which has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of concurrent processes executing arbitrary C code. The paper highlights the limitations of existing state-space exploration techniques, which are restricted to analyzing systems where each state can be uniquely identified. The proposed search algorithm does not rely on this assumption, making it applicable to systems with complex state representations. The effectiveness of the new technique is demonstrated through an example where VeriSoft successfully discovered an error in a 2500-line C program controlling robots in an unpredictable environment. The paper also provides a detailed explanation of the concurrent system model, the dynamic semantics, and the state-space exploration techniques used, including the use of persistent sets and sleep sets to improve efficiency and reduce the risk of incompleteness in verification results.