2005
A computer checked algebraic verification of a distributed summation algorithm
Publication
Publication
Formal Aspects of Computing , Volume 17 - Issue 1 p. 19- 37
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.
| Additional Metadata | |
|---|---|
| , , , , , , | |
| Springer | |
| doi.org/10.1007/s00165-004-0052-7 | |
| Formal Aspects of Computing | |
| Organisation | Computer Security |
|
Groote, J. F., Monin, F., & Springintveld, J. G. (2005). A computer checked algebraic verification of a distributed summation algorithm. Formal Aspects of Computing, 17(1), 19–37. doi:10.1007/s00165-004-0052-7 |
|