LCS Publication Details
Publication Title: A LATTICE-STRUCTURED PROOF TECHNIQUE APPLIED TO A MINIMUM SPANNING TREE ALGORITHM
Publication Author: Welch, Jennifer L.
Additional Authors: Lamport, Leslie and Lynch, Nancy
LCS Document Number: MIT-LCS-TM-361
Publication Date: 6-1-1988
LCS Group: No Group Specified
Additional URL: No URL Given
Abstract:
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 non-modular 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 has until recently lacked a rigorous proof.
To obtain this publication:

    To purchase a printed copy of this publication please contact MIT Document Services.