We present an algebraic verification of Segall
s propagation of information with feedback algorithm and we report on the verification of the proof using the PVS system. This algorithm serves as a nice benchmark for verification exercises (see [2, 8, 17]). The verification is based on the methodology presented in [7] and demonstrates its suitability to deliver mechanically verifiable correctness proofs of highly nondeterministic distributed algorithms.
Keywords Distributed summation algorithm - Verification - Formal proof checking - Process algebra - 
CRL - PVS
The research of the second author was supported by Human Capital Mobility (HCM). The research of the third author was supported by the Netherlands Organization for Scientific Research (NWO) under contract SION 612-33-006.Received October 1988 by J. Rushby
Accepted September 2004 by C. B. Jones