Show simple item record

dc.contributor.advisorZemmari, Akka
dc.contributor.advisorCastéran, Pierre
dc.contributor.authorFONTAINE, Allyx
dc.contributor.otherChalopin, Jérémie
dc.date2014-06-16
dc.identifier.urihttp://www.theses.fr/2014BORD0091/abes
dc.identifier.urihttps://tel.archives-ouvertes.fr/tel-01127345
dc.identifier.nnt2014BORD0091
dc.description.abstractL’intérêt porté aux algorithmes probabilistes est, entre autres,dû à leur simplicité. Cependant, leur analyse peut devenir très complexeet ce particulièrement dans le domaine du distribué. Nous mettons en évidencedes algorithmes, optimaux en terme de complexité en bits résolvantles problèmes du MIS et du couplage maximal dans les anneaux, qui suiventle même schéma. Nous élaborons une méthode qui unifie les résultatsde bornes inférieures pour la complexité en bits pour les problèmes duMIS, du couplage maximal et de la coloration. La complexité de ces analysespouvant facilement mener à l’erreur et l’existence de nombreux modèlesdépendant d’hypothèses implicites nous ont motivés à modéliserde façon formelle les algorithmes distribués probabilistes correspondant ànotre modèle (par passage de messages, anonyme et synchrone), en vuede prouver formellement des propriétés relatives à leur analyse. Pour cela,nous développons une bibliothèque, RDA, basée sur l’assistant de preuveCoq.
dc.description.abstractEnProbabilistic algorithms are simple to formulate. However, theiranalysis can become very complex, especially in the field of distributedcomputing. We present algorithms - optimal in terms of bit complexityand solving the problems of MIS and maximal matching in rings - that followthe same scheme.We develop a method that unifies the bit complexitylower bound results to solve MIS, maximal matching and coloration problems.The complexity of these analyses, which can easily lead to errors,together with the existence of many models depending on implicit assumptionsmotivated us to formally model the probabilistic distributed algorithmscorresponding to our model (message passing, anonymous andsynchronous). Our aim is to formally prove the properties related to theiranalysis. For this purpose, we develop a library, called RDA, based on theCoq proof assistant.
dc.language.isofr
dc.subjectAlgorithme distribué
dc.subjectAssistant de preuve
dc.subjectPreuve formelle
dc.subjectAnalyse
dc.subjectAlgorithme probabiliste
dc.subject.enDistributed algorithm
dc.subject.enProof assistant
dc.subject.enFormal method
dc.subject.enAnalysis
dc.subject.enRandomised algorithm
dc.titleAnalyses et preuves formelles d'algorithmes distribués probabilistes
dc.title.enAnalyses and Formal Proofs of Randomised Distributed Algorithms
dc.typeThèses de doctorat
dc.contributor.jurypresidentMosbah, Mohamed
bordeaux.hal.laboratoriesLaboratoire bordelais de recherche en informatique
bordeaux.type.institutionBordeaux
bordeaux.thesis.disciplineInformatique
bordeaux.ecole.doctoraleÉcole doctorale de mathématiques et informatique (Talence, Gironde ; 1991-....)
star.origin.linkhttps://www.theses.fr/2014BORD0091
dc.contributor.rapporteurMéry, Dominique
dc.contributor.rapporteurRavelomanana, Vlady
bordeaux.COinSctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.title=Analyses%20et%20preuves%20formelles%20d'algorithmes%20distribu%C3%A9s%20probabilistes&rft.atitle=Analyses%20et%20preuves%20formelles%20d'algorithmes%20distribu%C3%A9s%20probabilistes&rft.au=FONTAINE,%20Allyx&rft.genre=unknown


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record