%0 Conference Proceedings
%T Une Analyse Formelle en Coq d'un Algorithme Distribué Probabiliste résolvant le Problème du Rendez-Vous
%+ Laboratoire Bordelais de Recherche en Informatique (LaBRI)
%A Fontaine, Allyx
%A Zemmari, Akka
%< avec comité de lecture
%B JFLA - Journées francophones des langages applicatifs
%C Aussois, France
%Y Damien Pous and Christine Tasson
%8 2013-02-03
%D 2013
%K Coq
%K Algorithme distribué probabiliste
%K Rendez-vous
%Z Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]Conference papers
%X 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.
%G French
%2 https://inria.hal.science/hal-00779700v1/document
%2 https://inria.hal.science/hal-00779700v1/file/jfla2013-08.pdf
%L hal-00779700
%U https://inria.hal.science/hal-00779700
%~ CNRS
%~ ENSEIRB
%~ UNIV-BORDEAUX
%~ JFLA2013
%~ JFLA