PADEC
Coq Library
Tools
PADEC - Coq Library

Model and General Results about the Model

Tool for Termination or Convergence

Tools for Composition

Tools for Complexity

Network Topologies

Toy examples of Network and Algorithm

Case Studies

Step Complexity: Diskstra's first token ring algorithm

k-Dominating Set Algorithm


Based on "Competitive Self-Stabilizing k-Clustering" . Focuses on the first rules of the second algorithms that build a k dominating set on a directed tree.

k-Clustering Algorithm


Based also on "Competitive Self-Stabilizing k-Clustering" . This proof extends the previous case study: we study the whole second algorithm (three rules) that builds a k clustering dominating set on of a spanning tree of the network.

Tools