Sciweavers

Share
IPPS
2002
IEEE

Proving Self-Stabilization with a Proof Assistant

11 years 4 months ago
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.
Pierre Courtieu
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where IPPS
Authors Pierre Courtieu
Comments (0)
books