A proof assistant is an appropriate tool to write sound proofs. The need of such tools in distributed computing grows over the years due to the scientific progress that leads algorithmic designers to consider always more difficult problems. In that spirit, the PADEC Coq library has been developed to certify self-stabilizing algorithms. Efficiency of self-stabilizing algorithms is mainly evaluated by comparing their stabilization times in rounds, the time unit that is primarily used in the self-stabilizing area. In this paper, we introduce the notion of rounds in the PADEC library together with several formal tools to help the certification of the complexity analysis of self-stabilizing algorithms. We validate our approach by certifying the stabilization time in rounds of the classical Dolev et al’s self-stabilizing Breadth-first Search spanning tree construction.

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 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 silent self-stabilizing algorithm which builds a $k$-clustering of the network. We also certify a quantitative property related to the output of this algorithm. Precisely, we show that the computed $k$-clustering contains at most $\lfloor \frac{n-1}{k+1} \rfloor + 1$ clusterheads, where $n$ is the number of nodes in the network. To obtain these results, we also developed a library which contains general tools related to potential functions and cardinality of sets.

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.