Groupe de travail: Preuves formelles d'algorithmes distribués

Salle 075, 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