Pour l'année 1999/2000, les séminaires du LIP auront lieu le mercredi après-midi à 13h30 deux fois par mois avec en alternance un exposé d'un intervenant local / un exposé d'un intervenant extérieur.
Ancien Responsable: Arnaud Tisserand
Renseignements et propositions d'exposés pour l'année 2001/2002
à : Nicolas Schabanel
Retour à la page du séminaire du LIP 2001/2002
Le contrôle de la qualité numérique et l'amélioration de la précision des résultats en Calcul Scientifique est nécessaire pour assurer la validité des modélisations numériques fines de problèmes physiques complexes et instables.
Une nouvelle méthode de correction automatique des erreurs d'arrondi, la méthode CENA, consiste à calculer exactement la contribution d'ordre un des erreurs d'arrondi élémentaires introduites par l'arithmétique flottante, dans l'erreur finale de toute chaîne de calculs. Une fois les hypothèses théoriques validées, cette correction utilise la différentiation automatique et le calcul de ces erreurs d'arrondi élémentaires. Des expérimentations numériques, conduites en Ada et en Fortran90, sur des algorithmes directs ou itératifs, valident l'efficacité de la méthode CENA pour stabiliser ces algorithmes et en améliorer la précision.
Après un rapide tour d'horizon des méthodes automatiques de contrôle de la qualité numérique des logiciels scientifiques, cet exposé sera centré sur la méthode CENA. Nous examinerons en particulier les hypothèses et limitations de la méthode, les différentes composantes de l'erreur résiduelle, certains aspects d'implantation ainsi que les différents modes d'application illustrés par des exemples d'algorithmes numériques.
Les microprocesseurs et les architectures parallèles d'aujourd'hui lancent de nouveaux défis aux techniques de compilation. En présence de parallélisme, les optimisations deviennent trop spécifiques et complexes pour être laissées au soin du programmeur. Les techniques de parallélisation automatique dépassent le cadre traditionnel des applications numériques et abordent de nouveaux modèles de programmes, tels que les nids de boucles non affines, les appels récursifs et les structures de données dynamiques. Des analyses précises sont au coeur de la détection du parallélisme, elles rassemblent des informations à la compilation sur les propriétés des programmes à l'exécution. Ces informations valident des transformations utiles pour l'extraction du parallélisme et la génération de code parallèle. Cet expose aborde principalement des analyses et des transformations avec une vision par instances, c'est-à-dire considérant les propriétés individuelles de chaque instance d'une instruction à l'exécution. Une nouvelle formalisation à l'aide de langages formels nous permet tout d'abord d'étudier une analyse de dépendances et de définitions visibles par instances pour programmes récursifs. L'application de cette analyse à l'expansion et la parallélisation de programmes récursifs dévoile des résultats encourageants.
Les intervalles constituent un moyen simple et naturel de représenter les nombres sur ordinateur. Ils permettent de tenir compte de l'erreur sur la représentation des données et d'éventuelles incertitudes sur la connaissance de celles-ci. Les arrondis dirigés nous permettent facilement d'obtenir des encadrements prouvés des résultats pour les algorithmes n'utilisant que +,*,/,et sqrt.
Malheureusement, il n'est pas simple de mener les calculs avec des intervalles et il est nécessaire de modifier profondément tous les algorithmes utilisés avec des données scalaires si on souhaite obtenir un encadrement final pas trop pessimiste.
Nous expliquerons quelles sont les sources de cette surestimation (sub-distributivité, effet enveloppant) et nous montrerons quelques techniques permettant d'obtenir des encadrements raisonnables.
Dans cet exposé, nous présentons le problème du consensus et rappelons le théorème établi par Fischer, Lynch et Paterson qui prouve qu'il est impossible de réaliser un consensus dans un système asynchrone où les processus sont susceptibles de tomber en panne. Nous présentons et comparons les différentes méthodes permettant de ``contourner'' ce résultat d'impossibilité : randomisation, modèles partiellement synchrones, détecteurs de défaillances, méthodes hybrides. Nous discutons l'impact de ces résultats dans les applications critiques telles que le contrôle aérien, la sûreté des centrales nucléaires, ...
Tiens, le produit de matrices ! Sur machines parallèles ou distribuées hétérogènes (dont les processeurs ne vont pas à la même vitesse), le problème se révèle difficile: au menu, NP-complétude, preuve, jolies heuristiques, et coucourbes expérimentales.
Travail réalisé en commun avec Olivier Beaumont, Vincent Boudet et Fabrice Rastello.
Lors de sa visite au Lip, Luc Moreau a exposé un algorithme distibué de comptage de références de son cru. Luc avait alors une preuve papier de la correction de cet algorithme. Nous avons écrit une version utilisant l'assistant de preuves Coq.
L'expose commencera par une présentation de l'algorithme distribué, suivi d'une présentation de la preuve de correction en Coq. Il se terminera par un point de vue plus personnel sur l'intérêt d'utiliser un logiciel de preuves pour écrire ses preuves et sur son coût, ce qui ouvrira le débat...
Les machines à vecteurs de support (Support Vector Machines) ont été développées dans les années 90 et font actuellement partie des méthodes statistiques les plus performantes pour traiter des problèmes réels. Cet exposé présente les bases théoriques de ces machines ainsi que les extensions qui les ont rendues populaires. On parlera en particulier de principes d'induction automatiques, du rapport entre analyse fonctionnelle et statistique, de minimisation quadratique sous contrainte, et tout cela en restant dans un cadre applicatif.
Quand on est petit, on aime bien les devinettes. Un des jeux favoris des cours de récré consiste à faire deviner un entier avec des questions comme <<est-ce 17 ?>>. En grandissant, on découvre qu'on peut aller plus vite en posant des questions comme <<Est-ce plus grand que 13 ?>>. Que se passe-t-il si on autorise plutôt les questions du style <<Est-ce une racine de x^2-30x+221 ?>> ? Et si on prend en compte la taille de la question ?
Continuons à prendre de l'âge et découvrons la dérivée, les puissances et les racines. Il faut maintenant deviner une puissance ou une racine d'un élément. La dérivée est un outil qui nous permet de poser des questions plus compliquées. Mais permet-elle vraiment de résoudre plus vite la devinette ?
Les méthodes de type Krylov/Lanczos, communes en calcul flottant, sont aussi utilisées depuis quelques années en calcul exact pour le traitement de grandes matrices creuses. Elles ont leur importance puisque le traitement de telles matrices (de dimension plusieurs centaines de milliers) est clé par exemple pour des problèmes de factorisation ou pour la résolution d'équations algébriques. Dans ce contexte, nous considérerons ces méthodes comme directes pour les appliquer à des problèmes de base de l'algèbre linéaire (résolution de systèmes, calcul de rang, du polynôme minimal, du polynôme caractéristique) avant tout sur des corps finis GF(q).
Nous nous proposons dans cet exposé d'aborder certains des problèmes/solutions étudiés tout à fait spécifiquement en calcul formel. Nous introduirons les algorithmes probabilistes utilisés. Nous insisterons sur la notion récente de pré-conditionnement algébrique qui, à l'instar de la notion numérique, s'utilise pour faciliter les calculs (mais n'a guère de vraiment en commun que le nom). En particulier, nous étudierons l'utilisation de matrices aléatoires creuses spéciales, comme pré-conditionneurs à faibles coûts valables mêmes sur des corps ayant très peu d'éléments comparé à la dimension du problème.
Dans cet exposé je présenterai d'abord deux techniques de l'algorithmique du mot -- les fonctions d'extension et la factorisation de Lempel-Ziv . La première représente un calcul efficace et utile dans les application, basé sur l'algorithme de Knuth-Morris-Pratt. La deuxième construit une factorisation du mot utilisée par ailleurs dans l'algorithme bien connu de compression. La construction se fait à l'aide de l'arbre de suffixes ou le DAWG (Directed Acyclic Word Graph) et je parlerai brièvement, si le temps me le permet, de ces structures.
Je montrerai ensuite comment ces techniques permettent de trouver rapidement toutes les répétitions dans un mot, aussi bien les répétitions successives (en tandem) que les répétitions à une distance donnée. Je parlerai également ici de propriétés combinatoires de répétitions, nécessaires dans l'analyse des algorithmes.
Je présenterai dans cet exposé un certain nombre de concepts et d'outils développés dans l'étude sémantique des systèmes parallèles. Je décrirai en particulier des approches visant à répondre aux questions suivantes:
Il sera notamment question d'algèbres de processus et de bisimulation, et je m'efforcerai de traiter quelques exemples, pour montrer comment les notions abordées sont utilisées.
Les traces locales sont une extension des traces de Mazurkiewicz permettant de décrire les comportements concurrents des réseaux de Petri non-saufs. Nous présentons à l'aide de l'exemple du Producteur-Consommateur une extension du théorème de Büchi pour les langages de traces locales: un langage de traces locales est reconnaissable (par un automate fini) si et seulement si ses processus sont définissables dans la logique monadique du second ordre et admettent une couverture finie. Ce travail généralise les résultats connus dans les cas particuliers des mots, des traces de Mazurkiewicz et des traces stables pour lesquels tout ensemble de processus admet une couverture finie.
Travail commun avec Dietrich Kuske.
Quelques données internes sur notre séminaire (accès LIP uniquement).
Last modified: Fri Sep 29 09:56:16 MET DST 2000
Isabelle Guérin Lassous