Proving Self-Stabilization with a Proof Assistant

We present a formalization of a proof of self-stabilization in the Coq proof assistant. Coq is a program allowing to define mathematical objects and properties, and to make proofs on them in a certified way. We use it to formalize a generic proof of stabilization for algorithms running on a linear net or a ring [1]. In this method net configurations are considered as words and the algorithm as a rewriting system on words.

• Type: Conference
• Year: 2002
• Where: IPPS
• Authors: Pierre Courtieu
• Keywords: Coq Proof Assistant, Distributed And Parallel Computing, Generic Proof, IPPS 2002, Method Net Configurations