The task is to find a suitable model for verification purposes of distributed algorithms. As an example we verified the S algorithm of Chandra/Toug within the theorem proving environment Isabelle/HOL. We first designed a TLA+ model and adopted and extended this model to formally show the three consensus properties Validity, Agreement and Termination.
Safety- and Liveness Properties of Distributed Algorithms formally verified
- Written by Christoph Wagner
- Category: D-CON