Evènement pour le groupe Algorithmique Distribuée


Date 2012-02-13  14:00-15:00
TitrePreuves 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.  
Lieus. 076 
OrateurAllyx Fontaine 



Aucun document lié à cet événement.

Retour
Retour à l'index