A Framework for Certified Self-Stabilization

Karine Altisen, Pierre Corbineau, Stephane Devismes

We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory m…