February – 2009

The celebrated Minimum Spanning Tree protocol of Gallager, Humblet and Spira has been very influential in the network algorithms arena. Although it is very intuitive it has proven to be a very hard protocol to verify correct. Despite many attempts, only two proofs were previously known, each roughly 180 pages long. We describe a new proof of correctness that is considerably shorter, and is the first to formalize the reasoning suggested in the original paper. The proof is based on a new abstraction that facilitates modular reasoning about the protocol. The talk will be self contained and will assume no prior knowledge of the subject matter.

Based on joint work with Benny Shimony.