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):

Download

The code has been written using Coq Version 8.8.0, compiled with OCaml 4.08.1 The whole development mainly includes Coq source code with every definition and proof involved in the framework and case studies.

Publication