Home > Research > Publications & Outputs > Brief announcement: MP-state


Text available via DOI:

View graph of relations

Brief announcement: MP-state: State-aware software model checking of message-passing systems

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Publication date2012
Host publicationStabilization, Safety, and Security of Distributed Systems: 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings
Number of pages4
Volume7596 LNCS
<mark>Original language</mark>English


Software model checking [4] 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 [6]. 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 [2]. Intuitively, state capture enables to detect that two states are identical and, therefore, to consider only a representative state for verification. Unfortunately, capturing the state in general software systems can be very hard, even if the entire state of the system resides in the (local) memory. As a result, certain verification approaches (commonly called stateless model checking) do not capture the system's state at all [4]. Stateful model checking is in principle possible for software, however, at a price of considerable overhead. Therefore, stateful model checking is efficient only if the achieved reduction of redundantly explored states compensate for the overhead. © 2012 Springer-Verlag.