We propose a framework, based on Coq, to (semi-) automatically construct certified proofs of self-stabilizing algorithms called PADEC. The framework imports into Coq the computational model in which the algorithms are designed, formalizes the algorithms themselves and their specifications. Then the algorithms are proved using Coq including safety, convergence. The current development of the framework includes performance studies and complexity proofs but also connection with other formal tools.
The goal of the proposed research is to provide a decision procedure for the Coq proof assistant that would extend equality-based reasoning (i.e. the congruence tactic) to heterogeneous problems where equalities are expressed using multiple equivalence relations (i.e. setoids).