Proving self-stabilization with a proof assistant
Pierre Courtieu · 2002
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.