Lattice-structured proof technique applied to a minimum spanning-tree algorithm. Technical report
Jennifer Lundelius Welch, Leslie Lamport, N. Lynch · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1988
Highly-optimized concurrent algorithms are often hard to prove correct because they have no natural decomposition into separately provable parts. This paper presents a proof technique for the modular verification of such nonmodular algorithms. It generalizes existing verification techniques based on a totally-ordered hierarchy of refinements to allow a partially-ordered hierarchy - that is, a lattice of different views of the algorithm. The technique is applied to the well-known distributed minimum spanning-tree algorithm of Gallager, Humblet and Spira, which was until recently lacked a rigorous proof.