Groupe de travail: Preuves formelles d'algorithmes distribués
Salle 381, Le jeudi de 9h30 à 10h30.
Ce groupe s'intéresse principalement à la preuve assistée d'algorithmes
distribués présentés sous forme de calculs locaux
(systèmes de réétiquetage
dans un graphe (voir par exemple cet article et l'outil
Visidia).
Nous construisons un environnement de preuve sur les calculs locaux où
la métathéorie est exprimée dans le calcul des constructions inductives
en utilisant l'assistant de preuves Coq.
Le générateur d'obligations de preuves
Outre l'algorithmique distribuée et sa modélisation, ce groupe s'intéresse
à tous les aspects de la preuve interactive en logique d'ordre supérieur.
Programme 2010-2011
- 7 octobre 2010:
Allyx Fontaine
Représentation de graphes en Coq.
- 30 septembre 2010:
Akka Zemmari
Suite du cours sur les algorithmes
distribués probabilistes.
- 23 septembre 2010:
Vincent Filou
Une preuve d'algorithme de construction d'arbre recouvrant
- 16 septembre 2010:
Akka Zemmari d&ecute,bute une série de 3 cours sur les algorithmes
distribués probabilistes.
Les transparents
Responsable : Pierre Castéran
pierre dot casteran at labri dot fr