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