Home > Verimag > Projects

PADEC

AGIR-Pôle-MSTIC 2015

Sommaire

Internship Opportunities

Silent Self-Stabilizing Algorithms: Certification Using Coq

Scientific Context

Modern distributed systems can be large-scale, dynamic, and / or resource constrained. These characteristics make them more vulnerable to faults. Now, the scale of these systems as well as the adversarial environment where they may be deployed limit the possibility of human intervention to repair them. In this context, fault-tolerance, i.e., the ability of a distributed algorithm to withstand faults, is mandatory.

Self-stabilization is a versatile lightweight technique to withstand transient faults in a distributed system: a self-stabilizing algorithm recovers correct behavior within finite time after transient faults. Self-stabilization makes no hypotheses on the nature or extent of transient faults that could hit the system, and recovers from the effects of those faults in a unified manner. Therefore the property of self-stabilization is very attractive for a distributed algorithm.

The correctness of self-stabilizing algorithms is often tricky to establish. It is even more complex and subtle as today’s research on self-stabilizing focuses on more adversarial environments. Now, the proof that a distributed algorithm actually achieves a self-stabilizing property is usually performed by hand, using informal reasoning. Such methods are clearly pushed to their limits. This justifies the use of a proof assistant, a program which allows to mechanically verify proofs. Proof assistants are environments where a user can express programs, state theorems, and develop proofs interactively, those ones being mechanically checked (that is, machine-checked). In this project, we use the Coq proof assistant.

Project Summary

PADEC aims at supporting an emerging collaboration between three researchers. The long-term goal of the collaboration is to propose a framework, based on Coq, to (semi-) automatically construct certified proofs of self-stabilizing properties. Such a framework will have to be applicable to a large set of existing algorithms implementing self-stabilizing properties. Of course, this framework should propose techniques to address correctness (including termination) of algorithms, but also quantitative properties, such as bounds on the stabilization time and optimality of the computed solutions. The aforementioned techniques should be applicable to specific algorithms as well as large classes of algorithms, e.g., expressed as parametric algorithms or composite algorithms. We also want to consider more theoretical results such as lower complexity bounds, impossibility results, and necessary conditions for different classes of self-stabilizing algorithms.

Keywords: Distributed Algorithms, Self-Stabilization, Certified Proofs, Coq.