Evènement pour le groupe Algorithmique Distribuée

Date 2018-03-05  14:00-15:00
TitrePADEC: A Framework for Certified Self-Stabilization 
RésuméJoint work with Pierre Corbineau and Stéphane Devismes Self-stabilization is a property that allows distributed algorithms to withstand transient faults and recover a correct behavior within finite time. It has been introduced by Dijkstra in 1974. Over the last decades, progress in self-stabilization has led to consider more and more adversarial environments. This make the design, proof for correctness and complexity analysis of self-stabilizing solutions more and more intricate. However, those proofs are commonly written by hand, based on informal reasoning. In this work, we propose instead to use a proof assistant, a tool which allows to develop certified proofs interactively and check them mechanically. We present the PADEC framework, a Coq library dedicated to building certified proofs of self-stabilizing algorithms. We first define in Coq the computational model which is the most commonly used in the self-stabilizing area, and its semantics. We propose several tools for proving convergence of algorithms and for counting elements. We illustrate the use of our framework by: - certifying a non-trivial part of an existing self-stabilizing algorithm; - certifying a commonly-used composition operation for self-stabilizing algorithms. 
OrateurKarine Altisen 
UrlU. Grenoble 

Aucun document lié à cet événement.

Retour à l'index