Brief Announcement: MP-State: State-Aware Software Model Checking of Message-Passing Systems

Software model checking is a useful and practical branch of verification for verifying the implementation of the system. The wide usability comes at a price of low time and space efficiency. In fact, model checking of even simple single-process programs can take several hours using state-of-the-art techniques. Verification complexity gets even worse for concurrent programs that simultaneously execute loosely coupled processes. Verification efficiency can be greatly improved by capturing the state of the program, a technique generally referred to as stateful model checking. Intuitively, state capture enables to detect that two states are identical and, therefore, to consider only a representative state for verification.