The Coq mailing list

[Marie Duflot <duflot AT lsv.ens-cachan.fr>]

Bonjour,

J'ai le plaisir de vous annoncer que je soutiendrai ma thèse le lundi 15 
septembre à 14h à l'ENS de Cachan, salle de conférence du Pavillon des 
Jardins.

La soutenance aura lieu devant un jury composé de :

Joffroy Beauquier
Ahmed Bouajjani
Laurent Fribourg
Marta Kwiatkowska
Catuscia Palamidessi
Claudine Picaronny

La thèse s'intitule :

Algorithmes distribués sur des anneaux paramétrés - 
Preuves de convergence probabiliste et déterministe.


Cette thèse se situe dans le cadre de la vérification de systèmes
distribués ( machines organisées en réseau). 
Plus précisément, nous nous intéressons aux méthodes de preuve de convergence 
d'algorithmes distribués s'exécutant sur des réseaux en anneau de taille 
paramétrée. La convergence est une propriété assurant que l'algorithme 
atteint 
toujours (ou avec probabilite 1 dans le cadre probabiliste) un etat legitime 
(c'est à dire satisfaisant une certaine propriété).
La difficulté principale est d'obtenir des preuves de convergence valides
quelle que soit la taille du réseau et quelque soit l'ordre dans lequel
sont activees les machines (ordonnancement). 
Nous proposons un cadre formel qui permet de simplifier des methodes de 
preuves existantes.

Les principaux résultats sont les suivants.

- Dans le cadre des algorithmes probabilistes, nous avons exhibé un
critère local de convergence permettant de démontrer la convergence
d'algorithmes, quel que soit l'ordonnancement.

- En appliquant notre méthode à l'algorithme du dîner des philosophes
probabilistes, nous avons montré que l'hypothèse d'équité sur les machines,
considérée jusqu'ici comme nécessaire pour démontrer la convergence, est 
superflue.
Nous avons de plus exprimé pour la première fois le temps moyen de
convergence de cet algorithme en nombre d'actions

- Dans le cas des algorithmes déterministes, nous avons amélioré
l'automatisation d'une méthode de preuve de convergence fondée
sur la réécriture (en utilisant une stratégie de réécriture préfixe).
Nous avons ainsi démontré automatiquement la convergence de plusieurs
algorithmes, tirés notamment du domaine de l'auto-stabilisation.


Le plan d'accès se trouve à l'adresse suivante :

http://www.lsv.ens-cachan.fr/info-acces.php

Le Pavillon des Jardins est indiqué sur le deuxième plan.

-- 
Marie.