Evènement pour le groupe
Algorithmique Distribuée
Date | 2012-02-13 14:00-15:00 |
Titre | Preuves formelles d'algorithmes distribués probabilistes |
Résumé | Afin de prouver des propriétés d'algorithmes distribués probabilistes à l'aide d'un assistant de preuve tel Coq, il faut un modèle permettant de raisonner à la fois sur l'aspect distribué et sur le probabiliste. Une nouvelle méthode a été introduite dans la bibliothèque Alea concernant l'aspect probabiliste. Elle est basée sur l'interprétation monadique des programmes probabilistes vus en tant que distributions probabilistes.
Nous présentons en premier lieu comment l'interprétation des algorithmes probabilistes comme des distributions a permis de constituer la bibliothéque Alea de preuves formelles de propriétés de ces programmes. Nous verrons ensuite les choix faits pour modéliser les algorithmes distribués. Nous appliquerons enfin ces théories dans les cas de la brisure de symétrie, du handshake et du maximal matching.
|
Lieu | s. 076 |
Orateur | Allyx Fontaine |
Aucun document lié à cet événement.
RetourRetour à l'index