PADEC is a framework to build certified proofs of 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 self-stabilizing algorithm which builds a k-clustering of the network. We also certified a quantitative property related to its output: we show that the size of the computed k-hop dominating set is at most ⌊ (n-1)/(k+1) ⌋ + 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.
- [ACD16] A Framework for Certified Self-Stabilization. Karine Altisen, Pierre Corbineau, Stephane Devismes - FORTE'2016, the 36th IFIP International Conference on Formal Techniques for Distributed Objects, Components and System
- [AC17] Composition certifiee d'algorithmes autostabilisants silencieux. Karine Altisen, Pierre Corbineau - Algotel'2017, 19emes Rencontres Francophones sur les Aspects Algorithmiques des Telecommunications