dc.contributor.author | Welch, Jennifer Lundelius | en_US |
dc.contributor.author | Lamport, Leslie | en_US |
dc.contributor.author | Lynch, Nancy A. | en_US |
dc.date.accessioned | 2023-03-29T14:31:54Z | |
dc.date.available | 2023-03-29T14:31:54Z | |
dc.date.issued | 1988-06 | |
dc.identifier.uri | https://hdl.handle.net/1721.1/149143 | |
dc.description.abstract | Higly-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. | en_US |
dc.relation.ispartofseries | MIT-LCS-TM-361 | |
dc.title | A Lattice-structured Proof Technique Applied to a Minimum Spanning Tree Algorithm | en_US |
dc.identifier.oclc | 19318536 | |