Formal Proofs for Broadcast Algorithms

Authors: Mandy Zammit, Adrian Francalanza

Corresponding: Mandy Zammit (

Keywords: Distributed Algorithms, Broadcast Algorithms, Correctness


Issue: Xjenza Online Vol. 2 Iss. 2 - October 2014

Standard distributed algorithmic solutions to recurring distributed problems are commonly speci ed and described informally. A proper understanding of these distributed algorithms that clari es ambiguities requires formal descriptions. However, formalisation tends to yield complex descriptions. We formally study two broadcast algorithms and present an encoding framework using a process descriptive language and formalise these algorithms and their speci cations using this framework. Following these new formal encodings we discuss correctness proofs for the same algorithms.

Download Article: