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



Responsable : Pierre Castéran
pierre dot casteran at labri dot fr