%0 Conference Proceedings
%T A Framework for Certified Self-Stabilization
%+ Université Grenoble Alpes [2016-2019] (UGA [2016-2019])
%A Altisen, Karine
%A Corbineau, Pierre
%A Devismes, Stéphane
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Heraklion, Greece
%Y Elvira Albert
%Y Ivan Lanese
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9688
%P 36-51
%8 2016-06-06
%D 2016
%R 10.1007/978-3-319-39570-8_3
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01432926/document
%2 https://inria.hal.science/hal-01432926/file/426757_1_En_3_Chapter.pdf
%L hal-01432926
%U https://inria.hal.science/hal-01432926
%~ UGA
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9688
%~ UGA-COMUE