Home > Research > Publications & Outputs > Efficient verification of distributed protocols...


Text available via DOI:

View graph of relations

Efficient verification of distributed protocols using stateful model checking

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Publication date30/09/2013
Host publication2013 IEEE 32nd International Symposium on Reliable Distributed Systems
Number of pages10
ISBN (electronic)9780769551159
<mark>Original language</mark>English


This paper presents efficient model checking of distributed software. Key to the achieved efficiency is a novel stateful model checking strategy that is based on the decomposition of states into a relevant and an auxiliary part. We formally show this strategy to be sound, complete, and terminating for general finite-state systems. As a case study, we implement the proposed strategy within Basset/MP-Basset, a model checker for message-passing Java programs. Our evaluation with actual deployed fault-tolerant message-passing protocols shows that the proposed stateful optimization is able to reduce model checking time and memory by up to 69% compared to the naive stateful search, and 39% compared to partial-order reduction. © 2013 IEEE.