The verified incremental design of a distributed spanning
tree algorithm
In May, 1996, I concluded the construction of a mechanical proof
of the algorithm of Gallager, Humblet, and Spira for the
distributed determination of the minimumweight spanning tree of
an undirected graph of processes in which all edges have
different weights. See
R.G. Gallager, P.A. Humblet, P.M. Spira:
A distributed algorithm for minimumweight spanning trees.
ACM Trans. on Programming Languages and Systems, 5 (1983) 6677.
The proof is made with the theorem prover NQTHM1992 of Boyer and
Moore, which can be obtained from
nqthmrequest@cli.com, Computational Logic, Inc.,
1717 West Sixth Street, Suite 290,
Austin, Texas 78703, USA.
The algorithm, its design, and the construction of its proof
are described in
 W.H. Hesselink:
The verified incremental design of a distributed spanning
tree algorithm: extended abstract.
Formal Aspects of Computing 11 (1999) 4555.
 W.H. Hesselink:
The verified incremental design of a distributed spanning tree
algorithm. This full paper was stored in 1999 in an electronic
archive of Formal Aspects of Computing, but when the journal was taken
over by Springer V., the archive remained in Britain and was
subsequently lost. The present version was made from old sources in
February 2015.
The event files that can be read and submitted for NQTHM1992 to
yield the formal proof are

ghsAB.events contains the definitions needed to understand
the main theorems and to try the algorithm in NQTHM's
execution environment (827 lines)

ghsC.events contains some auxiliary definitions
and lemmas (350 lines)

ghsD.events contains the semantic lemmas, a
preparation for the proofs of invariance (894 lines)

ghsE.events contains the graph theory (2178 lines)

ghsF.events contains the theory needed to eliminate
the ghost variables from the algorithm (574 lines)

ghsJR.events contains the layers (Jq) through (Rq), yielding
the main results for safety (11805 lines)

ghsSY.events contains the layers (Sq) through (Yq),
the goal, progress, termination, and the preparations
for the conclusions (15335 lines)

ghsZ.events contains the final theorems (183 lines)
Latest update: 20 February, 2015. Comments and questions are welcome.
Back to my
home page.