**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

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.

### License

### Topics

### Session Heard_Of

- HOModel
- Reduction
- Majorities
- OneThirdRuleDefs
- OneThirdRuleProof
- UvDefs
- UvProof
- LastVotingDefs
- LastVotingProof
- UteDefs
- UteProof
- AteDefs
- AteProof
- EigbyzDefs
- EigbyzProof