Rectification: Soutenance de thèse de Idrissa SARR

Comme vous en avez probablement rendu compte, le 7 octobre est un jeudi au
lieu d'un lundi.

Désolé!
Idrissa SARR

Veuillez excuser pour les éventuels envois multiples.

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse qui aura lieu le
lundi 7 octobre 2010 à Jussieu dans la salle 211 (barre 55-65) à partir
de 14h.
http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/campus_jussieu2.html

Vous êtes également invités au pot qui suivra.

Titre de la thèse :
"Routage de transactions dans une base de données à large échelle".

Jury

Directeur de thèse:
Anne Doucet Lip6

Encadrant:
Hubert Naacke Lip6

Rapporteurs:
Esther Pacitti LIRMM
Rachid Guerraoui EPFL

Examinateurs:
Pierre Sens Lip6
Gabriel Antoniu INRIA
Stepéhane Gançarski LIp6
Samba Ndiaye UCAD

Résumé
La réplication dans les bases de données a été largement étudiée, au cours
des trois dernières décennies. Elle vise à améliorer la disponibilité des
données et à augmenter la performance d'accès aux données. Un des défis
majeurs de la réplication est de maintenir la cohérence mutuelle des
répliques, lorsque plusieurs d'entre elles sont mises à jour,
simultanément, par des transactions.

Des solutions qui relèvent partiellement ce défi pour un nombre restreint
de bases de données reliées par un réseau fiable existent. Toutefois, ces
solutions ne sont pas applicables à large échelle. Par ailleurs,
l'antinomie entre les besoins de performances et ceux de cohérence étant
bien connue, l'approche suivie dans cette thèse consiste à relâcher les
besoins de cohérence afin d'améliorer la performance d'accès aux données.

Dans cette thèse, nous considérons des applications transactionnelles
déployées à large échelle et dont les données sont hébergées dans une
infrastructure très dynamique telle qu'un système pair-à-pair.
Nous proposons une solution intergicielle qui rend transparente la
distribution et la duplication des ressources mais aussi leur
indisponibilité temporaire. Nous définissons deux protocoles pour
maintenir la cohérence globale : un premier protocole ordonne les
transactions à partir de la définition a priori des données accédées, et
un deuxième qui détermine un ordre plus souple, en comparant les données
accédées, le plus tardivement possible, juste avant la validation des
transactions.
Toutes les solutions proposées tolèrent les pannes franches,
fonctionnalité essentielle pour que les résultats de cette thèse puissent
être mis en œuvre à très large échelle.
Finalement, nous avons implémenté nos solutions pour les valider
expérimentalement. Les tests de performances montrent que la gestion des
métadonnées est efficace et améliore le débit transactionnel et que la
redondance de l'intergiciel diminue le temps de réponse face aux
situations de pannes.

Idrissa Sarr
--
Ph.D. Student
Laboratoire d'Informatique de Paris 6
Tel SN: +221 775 236 257
Tel FR: +3 1 44 27 87 56
http://www-poleia.lip6.fr/~sarr

--
Ph.D. Student
Laboratoire d'Informatique de Paris 6
Tel SN: +221 775 236 257
Tel FR: +3 1 44 27 87 56
http://www-poleia.lip6.fr/~sarr

Soutenance de thèse de Idrissa SARR

Veuillez excuser pour les éventuels envois multiples.

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse qui aura lieu le
lundi 7 octobre 2010 à Jussieu dans la salle 211 (barre 55-65) à partir
de 14h.
http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/campus_jussieu2.html

Vous êtes également invités au pot qui suivra.

Titre de la thèse :
"Routage de transactions dans une base de données à large échelle".

Jury

Directeur de thèse:
Anne Doucet Lip6

Encadrant:
Hubert Naacke Lip6

Rapporteurs:
Esther Pacitti LIRMM
Rachid Guerraoui EPFL

Examinateurs:
Pierre Sens Lip6
Gabriel Antoniu INRIA
Stepéhane Gançarski LIp6
Samba Ndiaye UCAD

Résumé
La réplication dans les bases de données a été largement étudiée, au cours
des trois dernières décennies. Elle vise à améliorer la disponibilité des
données et à augmenter la performance d'accès aux données. Un des défis
majeurs de la réplication est de maintenir la cohérence mutuelle des
répliques, lorsque plusieurs d'entre elles sont mises à jour,
simultanément, par des transactions.

Des solutions qui relèvent partiellement ce défi pour un nombre restreint
de bases de données reliées par un réseau fiable existent. Toutefois, ces
solutions ne sont pas applicables à large échelle. Par ailleurs,
l'antinomie entre les besoins de performances et ceux de cohérence étant
bien connue, l'approche suivie dans cette thèse consiste à relâcher les
besoins de cohérence afin d'améliorer la performance d'accès aux données.

Dans cette thèse, nous considérons des applications transactionnelles
déployées à large échelle et dont les données sont hébergées dans une
infrastructure très dynamique telle qu'un système pair-à-pair.
Nous proposons une solution intergicielle qui rend transparente la
distribution et la duplication des ressources mais aussi leur
indisponibilité temporaire. Nous définissons deux protocoles pour
maintenir la cohérence globale : un premier protocole ordonne les
transactions à partir de la définition a priori des données accédées, et
un deuxième qui détermine un ordre plus souple, en comparant les données
accédées, le plus tardivement possible, juste avant la validation des
transactions.
Toutes les solutions proposées tolèrent les pannes franches,
fonctionnalité essentielle pour que les résultats de cette thèse puissent
être mis en œuvre à très large échelle.
Finalement, nous avons implémenté nos solutions pour les valider
expérimentalement. Les tests de performances montrent que la gestion des
métadonnées est efficace et améliore le débit transactionnel et que la
redondance de l'intergiciel diminue le temps de réponse face aux
situations de pannes.

Idrissa Sarr
--
Ph.D. Student
Laboratoire d'Informatique de Paris 6
Tel SN: +221 775 236 257
Tel FR: +3 1 44 27 87 56
http://www-poleia.lip6.fr/~sarr

Soutenance de thèse d'Ivan Noyer

Bonjour,

J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :

" Trois études sur l'implantation des matrices en FoCaLiZe, les
preuves quantitatives et la
réutilisation de preuves"

qui aura lieu le 28 septembre à 10h, campus de Jussieu tour 25-26, salle 101.

Le jury sera composé de:
Directeur de thèse:
M. Renaud Rioboo (ENSIIE)

Rapporteurs:
M. Gilles Dowek (LIX)
M. Choukri-Bey Ben Yelles (IUT Valence)

Examinateurs:
Mme. Alessandra Carbone (CNRS-UPMC)
M. Jacques Carette (McMaster University)
M. Roberto Di Cosmo (PPS)
M. Claudio Sacerdotti Coen (University of Bologna)

Résumé :

L'environnement de développement sûr FoCaLize
(http://focalize.inria.fr/) permet l'écriture de spécifications,
l'implantation de méthodes et l'écriture de la preuve de l'adéquation
d'un code à sa spécification.

Cette thèse part de la volonté d'implanter une bibliothèque de
matrices dans FoCaLize. Nous proposons une spécification dans laquelle
toutes les matrices sur un même anneau commutatif unitaire sont vues
comme des éléments d'une algèbre unitaire unique. Dans un tel
contexte, les opérateurs d'addition et de multiplication sont des
fonctions totales. Cela permet de les coder par des méthodes
récursives dans un type de données ne tenant pas compte de la
dimension des matrices.

Nous nous sommes ensuite intéressés au problème de la
recherche de spécifications dans la bibiothèque FoCaLize, laquelle est
considérée comme une base de données de formules du premier ordre
(prouvées ou non). La recherche d'une spécification aboutit s'il
existe une formule de la bibliothèque dont l'information cherchée soit
une conséquence dans un certain fragment de la logique du premier
ordre. Ce fragment est celui des preuves dites "quantitatives". Ces
dernières sont des preuves n'utilisant que les règles de
quantification du calcul des séquents et se terminant par la règle
axiome. Nous établissons un critère nécessaire et suffisant pour la
réussite de notre recherche, retrouvant ainsi un résultat connu. Nous
donnons deux formalisations équivalentes de notre critère. Nous
caractérisons ensuite l'admissibilité de la règle de coupure dans
notre fragment de la logique par une méthode que nous pensons originale.

Dans la foulée nous mettons en évidence une condition
nécessaire et suffisante pour qu'une modification des symboles
fonctionnels et relationnels dans un séquent du premier ordre permette
d'obtenir un nouveau séquent possédant une preuve quantitative. Nous
utilisons ce résultat pour proposer une méthode de réutilisation de
preuve par analogie dans la lignée de travaux antérieurs.

Finalement, nous décrivons informellement comment utiliser ces
résultats concernant la logique du premier dans le cadre de
l'environnement FoCaLiZe.

[mutekh-users] Soutenance de thèse Alexandre Becoulet

Bonjour,

J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée

"Conception d'un système d'exploitation supportant nativement les
architectures multiprocesseurs hétérogènes à mémoire partagée"

qui aura lieu le 28 septembre à 14h,
campus de Jussieu tour 25-26, salle 105.

Le jury sera composé de:

Directeur de thèse:
M. Alain Greiner (LIP6)

Encadrant de thèse:
M. Franck Wajsburt (LIP6)

Rapporteurs:
M. Paul Feautrier (ENS LYON)
M. Frédéric Pétrot (TIMA)

Examinateurs:
M. François Charot (INRIA)
M. Akim Demaille (Gostai)
M. Renaud Pacalet (ENST)
M. Pierre Sens (LIP6)

Résumé:

Cette thèse présente le système d'exploitation MutekH
(http://www.mutekh.org/), capable de s'exécuter nativement sur
une plateforme matérielle multiprocesseur, où les processeurs
peuvent être de complexité différente et disposer de
spécificités ou de jeux d'instructions différents.

Les travaux présentés ici s'insèrent dans un contexte où les systèmes
multi-core et les processeurs spécialisés permettent tous deux de
réduire la consommation énergétique et d'optimiser les performances
dans les systèmes embarqués et dans les systèmes sur puce.

Les autres solutions logicielles existantes permettant l'exécution
d'applications sur des plateformes multiprocesseurs hétérogènes
ne permettent pas, à ce jour, la communication par mémoire partagée,
telle qu'on l'envisage habituellement pour les systèmes
multiprocesseurs homogènes. Notre solution est la seule qui permet la
réutilisation du code source d'applications parallèles existantes pour
leur exécution directe par des processeurs différents.

La solution proposée est mise en oeuvre en deux phases: grâce au
développement d'un noyau dont l'abstraction rend
transparente l'hétérogénéité des processeurs, puis à la réalisation d'un
outil spécifique d'édition des liens, capable d'harmoniser le code et
les données des différents fichiers exécutables chargés en mémoire
partagée.

Les résultats obtenus montrent que MutekH permet l'exécution
d'applications préexistantes utilisant des services standards, tels que
les Threads POSIX, sur des plateformes multiprocesseurs hétérogènes
sans dégradation des performances par rapport aux autres systèmes
d'exploitation opérant sur des plateformes multiprocesseurs classiques.

--
Alexandre

Changement de salle pour la soutenance de thèse de Jean-Philippe Dubus

Bonjour,

Suite à un problème de transports, ma soutenance de thèse, intialement
prévue le jeudi 23 septembre à 14h dans l'amphi 25 aura finalement lieu
à la même date et à la même heure dans la salle de visioconférence de
l'atrium (rez-de-chaussée, entrée 2). Le pot qui suivra la soutenance
est par contre maintenu dans l'amphi 25, après délibération du jury.

Pour rappel des informations liées à la soutenance :

"Prise de décision multiattribut avec le modèle GAI"

=========
Résumé
=========

Les réseaux GAI sont une représentation graphique compacte et expressive
des préférences d'un décideur en Décision Multiattribut, c'est-à-dire
dans des situations où les alternatives sur lesquelles portent les choix
du décideur sont décrites à l'aide d'un ensemble d'attributs (de
caractéristiques). L'exploitation de leur structure graphique permet de
définir des procédures efficaces d'élicitation de préférences
(détermination des préférences à l'aide de questionnaires) ainsi que des
algorithmes assez performants de prise de décision (calcul de
l'alternative préférée du décideur ou des k meilleures alternatives).
Le but de cette thèse est double. Tout d'abord elle vise à étendre les
algorithmes de prise de décision dans des cas où les réseaux GAI sont
denses, c'est-à-dire dans des situations où leur structure ne permet pas
aux algorithmes de l'état de l'art de s'exécuter en un temps
raisonnable. Pour cela, une nouvelle méthode de triangulation approchée
a été développée, qui produit des réseaux GAI approchés sur lesquels des
mécanismes d'inférence adaptés permettent d'obtenir les alternatives
optimales des réseaux GAI d'origine. Ensuite, elle propose de nouvelles
méthodes d'inférence en Décision multicritère. Plus précisément, elle
propose des approches pour déterminer des frontières de Pareto (exactes
ou approchées avec garantie de performance) ou des frontières de Lorenz.
Elle propose également des algorithmes pour déterminer des solutions
optimales dans les cas où les critères peuvent être agrégés via des
opérateurs tels que OWA (Ordered Weighted Average), l'intégrale de
Choquet ou bien encore la norme de Tchebycheff.

=========
Abstract
=========

GAI networks are a graphical model, both compact and expressive, for
representing the preferences of a Decision Maker in the context of
Multiattribute Decision Making, i.e., in situations where the set of
alternatives among which the Decision Maker has to make decisions are
described as a set of attributes (or features). GAI network's graphical
structures are exploited to develop efficient elicitation procedures
(determination of the Decision Maker's preferences using questionnaires)
as well as effective Decision Making algorithms (e.g., computing the
preferred alternative or the k-best alternatives).
The goal of this PhD thesis is twofold. First, it extends the
aforementioned state-of-the-art Decision Making algorithms to be able to
cope with dense GAI networks, i.e., with situations where the GAI
network's treewidth is too high for these algorithms to complete in a
reasonable amount of time. For this purpose, a new triangulation method
has been developed which produces approximated GAI networks on which
tailored inference mechanisms determine the alternatives that are
actually optimal for the original GAI network. Second, we have proposed
new inference algorithms for Multicriteria Decision Making. More
precisely, new approaches for determining Pareto-optimal sets (exact and
approximate with performance guarantee) and Lorenz-optimal sets have
been developed. In addition, we have also proposed new algorithms for
computing the optimal solutions in situations where criteria are
aggregated using various operators like OWA (Ordered Weighted Average),
Choquet integrals and Tchebycheff's norm.

========
Jury
========

- Christophe GONZALES, Professeur à l'Université Pierre et Marie Curie
(directeur de thèse)
- Philippe LERAY, Professeur à l'Université de Nantes (rapporteur)
- Régis SABBADIN, Chargé de recherche INRA (rapporteur)
- Nicolas MAUDET, Maître de conférence à l'Université Paris Dauphine
(examinateur)
- Alix MUNIER-KORDON, Professeur à l'Université Pierre et Marie Curie
(examinateur)
- Patrice PERNY, Professeur à l'Université Pierre et Marie Curie
(examinateur)

========
Accès
========
Plan du campus : http://www.rhs.upmc.fr/plan2004.pdf

Soutenance de thèse de Fabien BONNEFOI

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse intitulée :

"Vérification Formelle des Spécifications de Systèmes Complexes,
Application aux Systèmes de Transport Intelligents"

La soutenance se déroulera:

==========
Lundi 27 Septembre à 14h00
à l'UPMC, 4 place Jussieu
bâtiment 41, salle 203-205.
Plan:
http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/campus_jussieu2.html
==========

Vous êtes également invités au pot qui suivra.

==========
RÉSUMÉ
==========

Les Systèmes de Transport Intelligent (STI) pour la route sont
indispensables à la gestion du trafic et à la sécurité des usagers.
Complexes et critiques, leur comportement dépend de nombreux
phénomènes continus et leur
conception nécessite la collaboration de nombreuses équipes. La
vérification formelle de ces systèmes pose différents problèmes
d'intégration au cycle de développement, d'explosion combinatoire,
de vérification des phénomènes continus et de coût de production des
modèles.

En utilisant le STI SAFESPOT comme cas d'étude, cette thèse propose
différentes solutions aux problèmes d'utilisation des méthodes
formelles au cours du cycle de développement d'un système complexe.
D'abord en proposant une méthode de génération de modèles formels à
partir des spécifications du système. Nous présentons un ensemble de
règles de transformation permettant de produire des modèles formels
(en Réseaux de Petri) à partir des spécifications semi-formelles du
système (des diagrammes UML). Cela permet de minimiser le coût de
production des modèles formels tout en favorisant une bonne
communication entre les différents acteurs d'un projet.

Différents aspects de composition du modèle formel sont ensuite étudiés afin
de permettre une approche modulaire. Grâce à l'élaboration d'un
patron générique pour notre modèle formel, différents scénarios de
composition et d'analyse peuvent être effectués à moindre coût tout
en réduisant les problèmes d'explosion combinatoire.

Enfin, nous proposons une technique d'intégration de phénomènes continus
dans les modèles formels par discrétisation. Cette approche permet
la production de modèles sur lesquels les propriétés de logique
temporelle sont décidables. Nous présentons une méthode de calcul de
la propagation des incertitudes liées à la discrétisation. Ces
incertitudes peuvent ensuite être prises en compte en modifiant les
modèles ou les propriétés à vérifier afin de garantir la validité
des preuves produites.

==========
ABSTRACT
==========

Intelligent Transportation Systems (STI) for the road are
essential for traffic management and security of road users.
Complex and critical, their behavior depends on many continuous
phenomena and their design requires the cooperation of many teams.
Formal verification of these systems raises several problems like
integration into a development cycle, combinatorial explosion,
verification of continuous phenomena and production costs of models.

Using SAFESPOT ITS as a case study, this thesis proposes
different solutions to integrate formal methods in the
development cycle of a complex system.
First, by proposing a method for generating formal models
from the system specifications. We present a set of
transformation rules to produce formal models
(in Petri nets) from semi-formal specifications of
system (UML diagrams). This minimizes the cost of
production of formal models while promoting good
communication between project stakeholders.

Different aspects of composition of formal model are then studied to
allow a modular approach. With the development of a
generic pattern for our formal model, different composition
and analysis scenarios can be performed at lower cost while
reducing the problems of combinatorial explosion.

Finally, we propose a technique for integrating continuous phenomena
in formal models by discretization. This approach allows
production models on which the properties in branching-time
logic is decidable. We present a method to compute
propagation of uncertainties related to the discretization. These
uncertainties can then be taken into account by modifying
models or verification properties to ensure
the validity of produced proofs.

==========
JURY
==========

Directeur de thèse:
M. Fabrice KORDON, Professeur à l'Université Pierre et Marie Curie
Rapporteurs:
M. Yvon KERMARREC, Professeur à l'École Nationale Supérieure des
Télécommunications de Bretagne
M. Jean-Claude ROYER, Professeur à l'École des Mines de Nantes
Examinateurs:
Mme. Béatrice BÉRARD, Professeur à l'Université Pierre et Marie Curie
Mme. Christine CHOPPY, Professeur à l'Université Paris Nord
M. Guy FREMONT, Innovative solutions manager
M. Franck POMMEREAU, Professeur à l'Université d'Évry

--
___________________________________
Fabien BONNEFOI
Doctorant Paris 6 / ATER Paris 13
Université Pierre & Marie Curie
Lip6 équipe Move
Bureau 202 tours 25-26
Tél.: +33 (0) 1 44 27 39 21
___________________________________

Soutenance de thèse de Jean-Philippe Dubus

Bonjour,

J'ai le plaisir de vous inviter à ma soutenance de thèse intitulée :
"Prise de décision multiattribut avec le modèle GAI"

La soutenance se déroulera le :

==========
Jeudi 23 Septembre à 14h00 à l'université Pierre et Marie Curie - 4
place Jussieu - 75005 Paris.
Dans l'amphithéâtre 25.
==========

Vous êtes également invités au pot qui suivra.

=========
Résumé
=========

Les réseaux GAI sont une représentation graphique compacte et expressive
des préférences d'un décideur en Décision Multiattribut, c'est-à-dire
dans des situations où les alternatives sur lesquelles portent les choix
du décideur sont décrites à l'aide d'un ensemble d'attributs (de
caractéristiques). L'exploitation de leur structure graphique permet de
définir des procédures efficaces d'élicitation de préférences
(détermination des préférences à l'aide de questionnaires) ainsi que des
algorithmes assez performants de prise de décision (calcul de
l'alternative préférée du décideur ou des k meilleures alternatives).
Le but de cette thèse est double. Tout d'abord elle vise à étendre les
algorithmes de prise de décision dans des cas où les réseaux GAI sont
denses, c'est-à-dire dans des situations où leur structure ne permet pas
aux algorithmes de l'état de l'art de s'exécuter en un temps
raisonnable. Pour cela, une nouvelle méthode de triangulation approchée
a été développée, qui produit des réseaux GAI approchés sur lesquels des
mécanismes d'inférence adaptés permettent d'obtenir les alternatives
optimales des réseaux GAI d'origine. Ensuite, elle propose de nouvelles
méthodes d'inférence en Décision multicritère. Plus précisément, elle
propose des approches pour déterminer des frontières de Pareto (exactes
ou approchées avec garantie de performance) ou des frontières de Lorenz.
Elle propose également des algorithmes pour déterminer des solutions
optimales dans les cas où les critères peuvent être agrégés via des
opérateurs tels que OWA (Ordered Weighted Average), l'intégrale de
Choquet ou bien encore la norme de Tchebycheff.

=========
Abstract
=========

GAI networks are a graphical model, both compact and expressive, for
representing the preferences of a Decision Maker in the context of
Multiattribute Decision Making, i.e., in situations where the set of
alternatives among which the Decision Maker has to make decisions are
described as a set of attributes (or features). GAI network's graphical
structures are exploited to develop efficient elicitation procedures
(determination of the Decision Maker's preferences using questionnaires)
as well as effective Decision Making algorithms (e.g., computing the
preferred alternative or the k-best alternatives).
The goal of this PhD thesis is twofold. First, it extends the
aforementioned state-of-the-art Decision Making algorithms to be able to
cope with dense GAI networks, i.e., with situations where the GAI
network's treewidth is too high for these algorithms to complete in a
reasonable amount of time. For this purpose, a new triangulation method
has been developed which produces approximated GAI networks on which
tailored inference mechanisms determine the alternatives that are
actually optimal for the original GAI network. Second, we have proposed
new inference algorithms for Multicriteria Decision Making. More
precisely, new approaches for determining Pareto-optimal sets (exact and
approximate with performance guarantee) and Lorenz-optimal sets have
been developed. In addition, we have also proposed new algorithms for
computing the optimal solutions in situations where criteria are
aggregated using various operators like OWA (Ordered Weighted Average),
Choquet integrals and Tchebycheff's norm.

========
Jury
========

- Christophe GONZALES, Professeur à l'Université Pierre et Marie Curie
(directeur de thèse)
- Philippe LERAY, Professeur à l'Université de Nantes (rapporteur)
- Régis SABBADIN, Chargé de recherche INRA (rapporteur)
- Nicolas MAUDET, Maître de conférence à l'Université Paris Dauphine
(examinateur)
- Alix MUNIER-KORDON, Professeur à l'Université Pierre et Marie Curie
(examinateur)
- Patrice PERNY, Professeur à l'Université Pierre et Marie Curie
(examinateur)

========
Accès
========
Plan du campus : http://www.rhs.upmc.fr/plan2004.pdf