Une Analyse Formelle en Coq d'un Algorithme Distribué Probabiliste résolvant le Problème du Rendez-Vous

Allyx Fontaine 1 Akka Zemmari 1
1 LaBRI - Laboratoire Bordelais de Recherche en Informatique
Résumé : Les algorithmes distribués probabilistes se formulent simplement, cependant leur analyse est complexe car il faut traiter à la fois l'aspect distribué et l'aspect probabiliste. Dans cet article, nous présentons une formalisation en Coq d'un algorithme distribué probabiliste résolvant le problème du rendez-vous. Cette formalisation nous permet de raisonner et de prouver des propriétés telles que la terminaison ou des calculs de probabilités.
Mots-clés : Coq Algorithme distribué probabiliste Rendez-vous
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00779700
Contributeur : Ist Inria Saclay <>
Soumis le : mardi 22 janvier 2013 - 14:50:42
Dernière modification le : mercredi 23 janvier 2013 - 15:02:33
Document(s) archivé(s) le : samedi 1 avril 2017 - 08:15:22

Fichier

jfla2013-08.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00779700, version 1

Collections

LABRI | UNIV-BORDEAUX | JFLA2013

Citation

Allyx Fontaine, Akka Zemmari. Une Analyse Formelle en Coq d'un Algorithme Distribué Probabiliste résolvant le Problème du Rendez-Vous. Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013. <hal-00779700>

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de
la notice

280

Téléchargements du document

307

Contact


archive-ouverte@inria.fr