PADEC is a framework to build certified proofs of self-stabilizing algorithms with the proof assistant Coq. The framework includes tools to model self-stabilizing algorithms, certified general statements that can be used to build certified correctness proofs of such algorithms, and case studies that validate them.
PADEC Online BrowsingSelf-extracted documentation from the development in Coq (proofs are omitted for readability):
- Current API: available here
DownloadThe code has been written using Coq Version 8.8.2, compiled with OCaml 4.07.0 The whole development in Coq includes all the definitions and proofs used in the framework and case studies.
- Current code: available here
- 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 System
- A Framework for Certified Self-Stabilization. Karine Altisen, Pierre Corbineau, Stéphane Devismes - Logical Methods in Computer Science (special issue of FORTE 2016)