Abstract : We exhibit a methodology to develop mechanically-checkable parameterized proofs of the correctness of fault-tolerant round-based distributed algorithms in an asynchronous message-passing setting. Motivated by a number of case studies, we sketch how to replace often-used informal and incomplete pseudo code by mostly syntax-free formal and complete definitions of a global-state transition system. Special emphasis is put on the required deepening of the level of proof detail to be able to check them within an interactive theorem proving environment.
https://hal.inria.fr/hal-01556227 Contributor : Hal IfipConnect in order to contact the contributor Submitted on : Tuesday, July 4, 2017 - 5:45:48 PM Last modification on : Monday, December 28, 2020 - 10:22:04 AM Long-term archiving on: : Sunday, December 17, 2017 - 1:17:36 PM