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.

Publication

PADEC Online Browsing

Self-extracted documentation from the development in Coq (proofs are omitted for readability):

Download

The code has been written using Coq Version 8.6, compiled with OCaml 4.04.1. The whole development in Coq includes all the definitions and proofs used in the framework and case studies.