Formal Proofs for Broadcast Algorithms
Mandy Zammit, Adrian Francalanza
Mandy Zammit (firstname.lastname@example.org)
Distributed Algorithms, Broadcast Algorithms, Correctness
Issue: Xjenza Online Vol. 2 Iss. 2 - October 2014
Standard distributed algorithmic solutions to recurring distributed problems are commonly specied and described informally. A proper understanding of these distributed algorithms that claries 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 specications using this framework. Following these new formal encodings we discuss correctness proofs for the same algorithms.