Abstract:

We provide a new proof of correctness for the celebrated
Minimum Spanning Tree protocol of Gallager, Humblet and Spira
(1983). Both the protocol and the quest for a natural
correctness proof have had considerable impact on the literature
concerning network protocols and verification. Our proof is 
based on a new intermediate-level abstraction of the protocol. 
The intermediate-level abstraction serves to prove structural 
properties on a simpler structure. Moreover, it is used as an 
auxiliary component in reasoning about the detailed algorithm. 
The outcome is the first proof that follows the spirit of the 
informal arguments made in the original paper.

The talk will not assume familiarity with the GHS algorithm or
knowledge of verification techniques. 

This is joint work with Benny Shimony.