Algebraic verification of a distributed summation algorithm
In this note we present an algebraic verification of Segall's Propagation of Information with Feedback (PIF) algorithm. This algorithm serves as a nice benchmark for verification exercises (see [2, 13, 8]). The verification is based on the methodology presented in  and demonstrates its applicability to distributed algorithms.
|Software/Program Verification (acm D.2.4), LOGICS AND MEANINGS OF PROGRAMS (acm F.3)|
|Specification and verification (program logics, model checking, etc.) (msc 68Q60), Theory of computing (msc 68Qxx)|
|Department of Computer Science [CS]|
Groote, J.F, & Springintveld, J.G. (1996). Algebraic verification of a distributed summation algorithm. Department of Computer Science [CS]. CWI.