Brief announcement: automated support for the design and validation of fault tolerant parameterized systems - a case study

We propose a methodology to use the infinite state model checker mcmt, based on the Satisfiability Modulo Theory technology, to assist in the design of fault tolerant algorithms. To prove the practical viability of our methodology, we applied it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg