Indeed, there have been numerous misunderstandings on what exactly a given algorithm is supposed to realize in what kinds of environments. Moreover, the abundance of subtly different computational models complicates comparisons between different algorithms. Charron-Bost and Schiper introduced the Heard-Of model for representing algorithms and failure assumptions in a uniform framework, simplifying comparisons between algorithms.
In this contribution, we represent the Heard-Of model in Isabelle/HOL. We define two semantics of runs of algorithms with different unit of atomicity and relate these through a reduction theorem that allows us to verify algorithms in the coarse-grained semantics (where proofs are easier) and infer their correctness for the fine-grained one (which corresponds to actual executions). We instantiate the framework by verifying six Consensus algorithms that differ in the underlying algorithmic mechanisms and the kinds of faults they tolerate.
@InProceedings{merz:heard-of-afp, author = {Henri Debrat and Stephan Merz}, title = {Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model}, journal = {Archive of Formal Proofs}, month = jul, year = 2012, note = {\url{http://afp.sf.net/entries/Heard_Of.shtml}, Formal proof development}, ISSN = {2150-914x}, }