A Framework for Certified Self-Stabilization
Karine Altisen, Pierre Corbineau, Stéphane Devismes · Lecture notes in computer science · 2016
We propose a framework to build certified proofs of self-stabilizing algorithms using the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity , the most commonly used model in the self-stabilizing area. We then validate our framework by certifying a non-trivial part of an existing self-stabilizing algorithm which builds a k -hop dominating set of the network. We also certify a quantitative property related to its output: we show that the size of the computed k -hop dominating set is at most \(\lfloor \frac{n-1}{k+1} \rfloor + 1\) , where n is the number of nodes. To obtain these results, we developed a library which contains general tools related to potential functions and cardinality of sets. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.