A computer checked algebraic verification of a distributed summation algorithm - Université de Bretagne Occidentale
Article Dans Une Revue Formal Aspects of Computing Année : 2005

A computer checked algebraic verification of a distributed summation algorithm

Résumé

Abstract. 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.

Dates et versions

hal-04702792 , version 1 (19-09-2024)

Identifiants

Citer

Jan Friso Groote, François Monin, Jan Springintveld. A computer checked algebraic verification of a distributed summation algorithm. Formal Aspects of Computing, 2005, 17 (1), pp.19-37. ⟨10.1007/s00165-004-0052-7⟩. ⟨hal-04702792⟩
6 Consultations
0 Téléchargements

Altmetric

Partager

More