A lattice-structured proof of a minimum spanning Conference Paper uri icon

abstract

  • 1988 ACM. 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 partiallyordered 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.

name of conference

  • Proceedings of the seventh annual ACM Symposium on Principles of distributed computing - PODC '88

published proceedings

  • Proceedings of the seventh annual ACM Symposium on Principles of distributed computing - PODC '88

author list (cited authors)

  • Welch, J. L., Lamport, L., & Lynch, N.

citation count

  • 14

complete list of authors

  • Welch, Jennifer L||Lamport, Leslie||Lynch, Nancy

publication date

  • January 1988