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
Document type :
Conference papers
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download
https://hal.inria.fr/hal-00779700
Contributor : Ist Inria Saclay <>
Submitted on : Tuesday, January 22, 2013 - 2:50:42 PM
Last modification on : Wednesday, May 23, 2018 - 9:12:01 PM
Long-term archiving on : Saturday, April 1, 2017 - 8:15:22 AM

File

jfla2013-08.pdf
Explicit agreement for this submission

Identifiers

  • 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. JFLA - Journées francophones des langages applicatifs, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00779700⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

406

Files downloads

418

Contact


archive-ouverte@inria.fr