Séminaires Croisés des Doctorants - Exposés 2002

Christophe Blondel
[Calendrier]

Directeur:
N. Ayache

Reconstruction 3D des Artères Coronaires par Appariement Trinoculaire

Jonathan Stoeckel
[Calendrier]

Directeur:
N. Ayache

Diagnostic precoce de la maladie d'Alzheimer par imagerie fonctionelle.

Je vous parlerai de methodes statistiques analysant l'image d'un sujet pour aider le diagnostic, et les pre-traitements necessaires a une telle analyse. Je parlerai plus specifiquement de la comparaison d'une image a un groupe d'images, et je discuterai les approches a base de statistical parametric mapping (SPM), de permutation, classification et de simulation. Ces travaux ont ete appliques a la detection de tumeurs dans des images MIBI-SPECT, la detection de lesions de sclerose en plaque dans des images IRM et la detection de la maladie d'Alzheimer dans des images HMPAO-SPECT.
Karen Brady
[Calendrier]

Directeur:
J. Zerubia

Segmentation of Textured Images

Two main issues arise when working in the area texture segmentation: the need to accurately describe the texture by adaptively capturing its underlying structure (in both the amplitude and the phase) and the need to perform analysis on the boundaries of textures. We tackle these problems within a consistent probabilistic framework. Starting from probability distributions on infinite images, we generate distributions on arbitrary finite regions by marginalization. For a Gaussian distribution, the computational requirement of diagonalization and the modeling requirement of adaptivity together lead naturally to adaptive wavelet packet models that capture the "significant amplitude features" in the Fourier domain. Undecimated versions of the wavelet packet transform can be used to diagonalize the Gaussian distribution efficiently, albeit approximately. We describe the implementation and application of this approach and then outline the use of boundary wavelets to remove one level of approximation and solve the boundary problem. We also briefly discuss the use of quartic terms in the energy to capture the phase relationships which are crucial to texture structure.
Raul ACOSTA-BERMEJO
[Calendrier]

Directeur:
Frederic Boussinot

REJO/ROS

REJO and ROS are two experimental tools built with the Reactive Approach. REJO is an extension of Java that generates objects which can be considered like Reactive Objects because they have their data and their reactive instructions. These objects might be considered too like Mobile Agents because they can migrate in a platform, named ROS, that provides the functionalities that they need. REJO and ROS are built over Junior, a set of Java class that gives the facility to make a reactive programming. The REJO's programming model, which is close to that of Junior, provides reactive instructions that are executed in a reactive machine. The set of reactive instructions implements the instantaneous broadcast events as well as a logic parallelism operator which does not use threads. One of the particularities of Junior reactive instructions is that they have a formal semantic defined by rewriting rules. The web page of REJO/ROS is http://www-sop.inria.fr/meije/rp/ROS/.
Pascal Zimmer
[Calendrier]

Directeur:
G. Boudol

Using Ambients to Control Resources

Current software and hardware systems, being parallel and reconfigurable, raise new safety and reliability problems, and the resolution of these problems requires new methods. Numerous proposals attempt at reducing the threat of bugs and preventing several kinds of attacks. In this talk, we develop an extension of the calculus of Mobile Ambients, named Controlled Ambients, that is suited for expressing such issues, specifically Denial of Service attacks, and we present a type system for Controlled Ambients, which makes resource control possible in our setting.
Nicolas Magaud
[Calendrier]

Directeur:
Yves Bertot

A GMP program computing square roots and its proof within Coq

We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann to compute square roots of arbitrary large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP) is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program.
Guillaume Dufay
[Calendrier]

Directeur: Gilles Barthes

Vérification Formelle de la Plate-forme JavaCard

Murrone Angelo
[Calendrier]

Directeur:
H. Guillard

Comportement du schéma de Godunov dans la limite des faibles nombres de Mach

On présente une analyse du comportement du schéma de Godunov dans la limite des faibles nombres de Mach. Nous étudions le problème de Riemann et montrons que la pression à l'interface entre deux cellules contient des ondes acoustiques d'ordre Mach même si les données initiales sont bien préparées et ne contiennent que des fluctuations de pression d'ordre Mach au carré. Nous proposons alors de modifier les flux calculés par les schémas de type Godunov en résolvant un problème de Riemann préconditionné au lieu du problème de Riemann original. Cette stratégie est appliquée à un solveur de type VFRoe et nous montrons qu'elle permet de retrouver un bon comportement de la pression. Des expériences numériques viennent confirmer ces résultats théoriques
Maud Meriaux
[Calendrier]

Directeur:
S. Piperno

Méthodes en maillages mobiles à topologie variable pour la résolution d'équations hyperboliques

Les problémes concrets en Méecanique des Fluides prescrivent souvent un maillage trèes raffin'e dans certaines zones (près des discontinuités par exemple). Suivant l'étendue de ces dernières, en général plus conséquente pour les écoulements instationnaires que stationnaires, le coût de calcul s'avère parfois prohibitif. Il semble alors naturel d'adapter dynamiquement le maillage à la solution afin de le réduire. Il faut ainsi faire bouger le maillage de manière adéquate et résoudre dans le même temps les équations initiales en maillage mobile. Cette deuxième partie qui demande la reformulation de l'équation de départ, est peu difficile pour des méthodes en volumes finis conservatives. Nous présentons ici une méthode numérique conservative, qui s'inspire du schéma de Godunov et dont la particularité est l'utilisation de maillages mobiles à topologie éventuellement variable (addition et soustraction de points). Le cadre de cet exposé sera celui des équations hyperboliques, linéaires ou non, en une dimension d'espace. Nous effectuons dans un premier temps une analyse numérique de la présente méthode. Pour plus de détails, nous renvoyons le lecteur à Nous déduisons de cette étude que les propriétés classiques de stabilité (principe du maximum, décroissance de la variation totale, stabilité L2) des schémas en volumes finis peuvent être conservées sous certaines hypothèses de type CFL. Ces dernières se révélent extrêmement restrictives sur le pas de temps dès que nous utilisons des maillages raffinés. Pour s'affranchir de ces limitations, nous introduisons un schéma en temps mixte explicite-implicite, qui tout en étant seulement localement implicite, préserve les propriétés citées ci-dessus. Dans un second temps, nous nous concentrons sur l'adaptation de maillage. Nous intégrons le schéma dans un code où les noeuds se déplacent de manière automatique. Pour ce faire, nous équidistribuons une fonction M sur l'ensemble des noeuds, puis nous incitons ces derniers à se déplacer à la vitesse du flux. Dans cette même perspective, nous couplons le maillage mobile avec des modifications de la topologie via un critère qui gère l'ajout et la suppression de noeuds. L'ajout de points correspond à une volonté de raffiner localement. La suppression permet de réduire le nombre de points inutiles. Finalement, nous présentons quelques exemples numériques simples afin d'illustrer les performances du schéma étudié.
Nicolas Canouet
[Calendrier]

Directeur:
L. Fezoui

Méthode Volumes Finis pour la résolution du système de Maxwell sur des grilles raffinées non-conformes

On s'intéresse ici à la résolution du système de Maxwell dans le domaine temporel. Les méthodes les plus populaires sont les méthodes Différences Finies, éléments finis et Volumes finis. Ces méthodes fiables peuvent engendrer des temps de calcul ou nécessiter une place mémoire très élevée lorsque des structures fines (fils, incrustations, .. ) interviennent. Une solution classique dans ces cas est l'emploi de grilles localement raffinées. Les méthodes sus-citées sont des schémas explicites dont la stabilité est assurée par une condition de type CFL. Dès lors que le maillage est raffiné, le pas de temps est imposé par le pas d'espace de la grille fine. Or ces méthodes sont très dispersives lorsque le pas de temps est éloigné du pas de temps optimal autorisé par la condition de stabilité. Nous proposons de répondre à ce problème par une méthode Volumes Finis. Les formulations Volumes Finis sont à même de traiter des grilles raffinées de manière non conforme. Nous modifions le schéma Volumes Finis Centrés (VFC) proposé par Malika Remaki en évaluant les flux par une interpolation dépendant d'un paramètre beta. Associé, à une approximation temporelle de type saute-mouton, nous construisons un schéma qui conserve un équivalent discret de l'énergie électromagnétique (pas de diffusion). Dans le cas mono-dimensionnel, nous montrons que pour tout pas de temps et pas d'espace compatibles avec la condition de stabilité, il existe un choix de beta tel que le beta-schéma associé soit d'ordre 4. Dans le cas du raffinement de maillage, nous choisissons localement le paramètre beta de telle sorte que le schéma soit localement d'ordre 4. Les phénomènes de dispersion sont alors maîtrisés. Nous obtenons de bons résultats même pour des raffinements 1:10 (ie le rapport entre les pas d'espace de la grille fine et la grille grossière est 10). Dans le cas bi-dimensionnel, cette approche ne peut nous conduire à un schéma d'ordre 4. Toutefois, nous sommes capables de déterminer localement le paramètre beta de telle sorte que l'erreur de dispersion soit minimisée. Les résultats sur des grilles conformes ou non-conformes restent très satisfaisants même pour un raffinement 1:10.