Model checking is a method for verifying the correctness of concurrent systems by exploring their state spaces. This paper presents a new approach to model checking that directly analyzes actual implementations of concurrent systems written in programming languages like C or C++. The approach uses a state-less search algorithm that explores the state space without storing intermediate states, making it more efficient for large systems. The algorithm is implemented in VeriSoft, a tool that systematically explores the state spaces of concurrent systems. VeriSoft can detect deadlocks, assertion violations, divergences, and livelocks in concurrent systems. It was successfully used to find an error in a 2500-line C program controlling robots in an unpredictable environment. The paper also discusses the limitations of traditional state-space exploration techniques and introduces partial-order methods to reduce the number of states and transitions explored. These methods, combined with state-less search, enable efficient verification of concurrent systems. The paper concludes that model checking is a powerful technique for verifying the correctness of concurrent systems, and that the new approach extends its applicability to programming languages.Model checking is a method for verifying the correctness of concurrent systems by exploring their state spaces. This paper presents a new approach to model checking that directly analyzes actual implementations of concurrent systems written in programming languages like C or C++. The approach uses a state-less search algorithm that explores the state space without storing intermediate states, making it more efficient for large systems. The algorithm is implemented in VeriSoft, a tool that systematically explores the state spaces of concurrent systems. VeriSoft can detect deadlocks, assertion violations, divergences, and livelocks in concurrent systems. It was successfully used to find an error in a 2500-line C program controlling robots in an unpredictable environment. The paper also discusses the limitations of traditional state-space exploration techniques and introduces partial-order methods to reduce the number of states and transitions explored. These methods, combined with state-less search, enable efficient verification of concurrent systems. The paper concludes that model checking is a powerful technique for verifying the correctness of concurrent systems, and that the new approach extends its applicability to programming languages.