Emplois et stages
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.