Loading...
Please wait, while we are loading the content...
Similar Documents
A Lattice-Structured Proof Technique Applied to a Minimum Spanning Tree Algorithm
| Content Provider | Semantic Scholar |
|---|---|
| Author | Welch, Jennifer L. Lamport, Leslie Lynch, Nancy A. |
| Copyright Year | 1988 |
| Abstract | 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 was until recently lacked a rigorous proof. Keywords: Distributed algorithms, Verification, Modularity, Partially ordered refinements, Liveness proofs, Minimum spanning tree. |
| File Format | PDF HTM / HTML |
| DOI | 10.21236/ada198312 |
| Alternate Webpage(s) | https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/A-Lattice-Structured-Proof-of-a-Minimum-Spanning-Tree-Algorithm.pdf |
| Alternate Webpage(s) | https://doi.org/10.21236/ada198312 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
