PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions.
PADEC Online Browsing
Self-extracted documentation from the development in Coq (proofs are omitted for readability):
- Current PADEC API available here
Download
The code has been written using Coq Version 8.15.0, compiled with OCaml 4.13.1 The whole development mainly includes Coq source code with every definition and proof involved in the framework and case studies.
- Current PADEC source code available here
Publication
- A Framework for Certified Self-Stabilization. Karine Altisen, Pierre Corbineau, Stéphane Devismes - FORTE'2016, the 36th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems
- A Framework for Certified Self-Stabilization. Karine Altisen, Pierre Corbineau, Stéphane Devismes - Logical Methods in Computer Science (special issue of FORTE 2016)
- Squeezing Streams and Composition of Self-Stabilizing Algorithms. Karine Altisen, Pierre Corbineau, Stéphane Devismes - FORTE'2019 - 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems
- Exact Worst Case Self-Stabilization Time. Karine Altisen, Pierre Corbineau, Stéphane Devismes - ICDCN 2021 - 22th International Conference on Distributed Computing and Networking.
- Certification of an exact worst-case self-stabilization time. Karine Altisen, Pierre Corbineau, Stéphane Devismes - Theoretical Computer Science - to appear.
- Certified Round Complexity of Self-Stabilizing Algorithms. Karine Altisen, Pierre Corbineau, Stéphane Devismes - DISC 2023 - International Symposium on Distributed Computing.