The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract

1 September 1999

journal article
research article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 11 (1) , 45-55
https://doi.org/10.1007/s001650050035

Abstract

: The paper announces an incremental mechanically–verified design of the algorithm of Gallager, Humblet, and Spira for the distributed determination of the minimum-weight spanning tree in a graph of processes. The processes communicate by means of asynchronous messages with their neighbours in the graph. Messages over one link may pass each other. The proof of the algorithm is based on ghost variables, invariants, and a decreasing variant function. The verification is mechanized by means of the theorem prover Nqthm of Boyer and Moore. This extended abstract is an introduction to the full paper that can be obtained by ftp (http://link.springer.de/link/service/journals/00165/).

Keywords

This publication has 5 references indexed in Scilit:

The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract
Formal Aspects of Computing, 1999
A mechanical proof of Segall's PIF algorithm
Formal Aspects of Computing, 1997
Distributed Algorithms
Published by Springer Nature ,1994
A lattice-structured proof of a minimum spanning
Published by Association for Computing Machinery (ACM) ,1988
A Distributed Algorithm for Minimum-Weight Spanning Trees
ACM Transactions on Programming Languages and Systems, 1983