HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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

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.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-00779700
Contributor : Ist Inria Saclay Connect in order to contact the contributor
Submitted on : Tuesday, January 22, 2013 - 2:50:42 PM
Last modification on : Monday, December 20, 2021 - 4:50:11 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

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⟩

Share

Metrics

Record views

257

Files downloads

279