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 [7] 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)
CWI
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.