Reference:

Loig Jezequel and Javier Esparza. Message passing algorithms for the verification of distributed protocols. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014, San Diego, USA, January 2014, To appear.

Abstract:

Message passing algorithms (MPAs) are an algorithmic paradigm for the following generic problem: given a system consisting of several interacting components, compute a new version of each component representing its behaviour inside the system. MPAs avoid computing the full state space by propagating minimal messages along the edges of the system interaction graph, when this graph is a tree. We present an MPA for verifying local properties of distributed protocols with a tree communication structure. We report on an implementation, and validate it by means of two case studies, including an analysis of the PGM protocol.

Suggested BibTeX entry:

@inproceedings{VMCAI14,
    author = {Loig Jezequel and Javier Esparza},
    booktitle = {Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2014, San Diego, USA, January 2014},
    title = {Message Passing Algorithms for the Verification of Distributed Protocols},
    year = {To appear}
}