# 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.
Type de document :
Communication dans un congrès
Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.36-51, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_3〉
Domaine :

Littérature citée [18 références]

https://hal.inria.fr/hal-01432926
Contributeur : Hal Ifip <>
Soumis le : jeudi 12 janvier 2017 - 11:34:43
Dernière modification le : jeudi 12 janvier 2017 - 11:38:42
Document(s) archivé(s) le : vendredi 14 avril 2017 - 15:16:37

### Fichier

##### Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

### Citation

Karine Altisen, Pierre Corbineau, Stéphane Devismes. A Framework for Certified Self-Stabilization. Elvira Albert; Ivan Lanese. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. Lecture Notes in Computer Science, LNCS-9688, pp.36-51, 2016, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-39570-8_3〉. 〈hal-01432926〉

### Métriques

Consultations de la notice