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 minimum-weight 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 minimum-weight spanning trees. ACM Trans. on Programming Languages and Systems, 5 (1983) 66-77.

The proof is made with the theorem prover NQTHM-1992 of Boyer and Moore, which can be obtained from nqthm-request@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

The event files that can be read and submitted for NQTHM-1992 to yield the formal proof are Latest update: 20 February, 2015. Comments and questions are welcome.

Back to my home page.