Nestmann, UweFuzzati, RacheleMerro, Massimo2005-11-232005-11-232005-11-23200310.1007/978-3-540-45187-7_26https://infoscience.epfl.ch/handle/20.500.14299/220555We give a process calculus model that formalizes a well known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (Diamond S); we use our model to formally prove that the algorithm satisfies its specification.Process CalculusModelFormalizationChandra-Toueg Consensus Algorithmtext::conference output::conference proceedings::conference paper