# A Framework for Certified Self-Stabilization

Abstract : 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$⌊n-1k+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.
Document type :
Conference papers
Domain :

Cited literature [18 references]

https://hal.inria.fr/hal-01432926
Contributor : Hal Ifip <>
Submitted on : Thursday, January 12, 2017 - 11:34:43 AM
Last modification on : Tuesday, May 11, 2021 - 11:36:25 AM
Long-term archiving on: : Friday, April 14, 2017 - 3:16:37 PM

### File

426757_1_En_3_Chapter.pdf
Files produced by the author(s)

### Citation

Karine Altisen, Pierre Corbineau, Stéphane Devismes. A Framework for Certified Self-Stabilization. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.36-51, ⟨10.1007/978-3-319-39570-8_3⟩. ⟨hal-01432926⟩

Record views