Semantic search
Mercredi 30 avril 2008, 14h-17h, Amphi 4
Mouldable Programming
- Documents
- mp.pdf
Magne Haveraaen, Institutt for Informatikk, Universitetet i Bergen, Norway
Mouldable programming is about looking at programs as mouldable
fragments of code, not as the static, brittle syntax software often
turns out to be. Some simple examples follow. The notation for calling
a method "push" which adds an element "E" to a stack "S" can be OO or
static method style, it can modify "S" or return the new stack
etc. Can we simplify usage to just one form, and mould it to the
actual call? A function which breaks down for some input can signal
this using return flags, special return values, or exceptions, to name
some common ways. Can we abstract over this, and mould to the relevant
error handling technique? Often we need to do run-time checking of
arguments, e.g., array indexing bounds, forcing us to introduce lots
of code to deal with the unwanted cases. Can we use mouldable ideas to
simplify the code? In the presentation, we will elaborate on such
examples, discussing how we can free us from awkward syntactic
constraints.
Magne Haveraaen is a professor of computer science with an interest
for programming technology: the theory and pragmatics of writing
code. He investigates this in the context of the Sophus software
library, a coordinate-free numerics library written in C++.
http://www.ii.uib.no/saga/
High-Level Abstractions and Optimization
Anya Helene Bagge, Institutt for Informatikk, Universitetet i Bergen, Norway
Writing code in an abstract, high-level style can cut development time
and make code more maintainable and easier to reason about - but at
the cost of lower run-time performance. For performance-critical
applications, such as in numerical programming, this can render modern
abstraction techniques infeasible. Fortunately, code that is easy for
humans to reason about is also easier to reason about
automatically. We're studying different abstraction mechanisms and
generative programming techniques, as well as optimization techniques
to produce efficient code for them. As an example, basic element-wise
operations on arrays may be expressed in terms of high-level
operations, which may be automatically combined in order to increase
performance. I will present some of the things we've been working on
so far, and some of the ideas we have for the future.
Anya Helene Bagge is a research fellow at the University of Bergen,
Norway. Her research interests include programming language design,
program transformation, parallel computer architectures and program
optimization.
http://www.ii.uib.no/~anya/
Mercredi 28 mai 2008, 14h-17h, Amphi 4
Le langage BSML
- Documents
- gava.pdf
Frédéric Gava, LACL, Université de Paris Est, Créteil
Nous présenterons BSML (Bulk Synchronous Parallel ML), un langage de
programmation de haut-niveau pour machines parallèles, ainsi que des
exemples classiques de parallélisme implémentés dans ce langage. Nous
complèterons cette présentation par une étude comparative des coûts
théoriques de ces algorithmes réalisée sur la grappe de PC du LACL.
Frédéric Gava est maître de conférences en informatique à
l'université de Paris 12. Ses travaux de thèse ont porté sur la
programmation parallèle (et des méta-ordinateurs) de haut-niveau qui
lui ont valu le prix de thèse 2006 de la fondation EADS dans le
domaine des STIC. Il travaille actuellement sur la preuve de
programme parallèle et la conception d'un vérificateur parallèle de
modèles pour réseaux de Petri de haut-niveau implanté avec les
méthodes développées lors de son travail de thèse.
http://lacl.univ-paris12.fr/gava/
Programmation parallèle certifiée
Frédéric Loulergue, LIFO, Université d'Orléans
L'algorithmique constructive permet, partant d'une spécification écrite
sous forme d'une combinaison non-efficace de fonctions, de dériver, sous
certaines conditions, des algorithmes parallèles efficaces. Cette dérivation
s'appuie sur des théorèmes d'équivalence de programmes et est formellement
correcte. Elle aide le programmeur à concevoir des programmes parallèles.
Toutefois les bibliothèques de squelettes proposées ne sont pas certifiées.
Dans le cadre d'une collaboration avec l'université de Tokyo, nous proposons
de cibler des squelettes algorithmiques développés en BSML et certifiés à
l'aide de l'assistant de preuve Coq.
Frédéric Loulergue est professeur à l'Université d'Orléans depuis
septembre 2005, directeur adjoint du Laboratoire d'Informatique
Fondamentale d'Orléans (LIFO), membre de l'équipe Parallélisme,
Réalité virtuelle et Vérification (PRV). Il travaille sur le
parallélisme avec des langages et modèles de haut-niveau (conception
de langages et bibliothèques, sémantique, vérification, algorithmes et
applications).
http://f.loulergue.free.fr/
Dimanche 14 septembre 2008, 14h-17h, Amphi 4
Systèmes, algorithmes et applications: Efficacité et utilité des systèmes parallèles.
- Documents
- hains.pdf
Gaétan Hains, LACL, Université de Paris Est, Créteil
Dans cet exposé je présenterai le modèle bulk-synchronous parallelism (BSP)
des algorithmes et architectures parallèles, ainsi qu'un tour d'horizon des
domaines d'application du parallélisme. BSP propose une vue unifiée des
principaux paramètres de la performance des algorithmes parallèles et de
leur adéquation sur les architectures multi-processeur, multi-coeur et leurs
réseaux de communication interne. Il permet une analyse portable et
extensible des performances ce qui permet d'éviter les principaux pièges de
l'informatique parallèle: mauvaise granularité, réseau mal adapté,
déséquilibres.
Gaétan Hains est directeur du LACL à l'université de Paris 12. Son
programme de recherche porte sur la programmation parallèle et la
sécurité.
http://lacl.univ-paris12.fr/hains
Outils pour le parallèlisme : apports de la programmation générative
- Documents
- falcou.pdf, falcou-1.pdf, falcou-2.pdf, falcou-3.pdf, falcou-4.pdf, falcou-5.pdf, falcou-6.pdf
Joël Falcou, IEF, Université de Paris-Sud, Orsay
Les besoins croissants en puissance de calcul exprimés par de nombreux domaines scientifiques exercent une pression très forte sur les architectures émergentes, les rendant toujours plus performantes mais toujours plus complexes à maîtriser. Dans ce cadre, le développement d'outils tirant parti des spécificités de ces architectures (quadri- et bientôt octo-coeurs, processeurs Cell ou GPU par exemple) devient une gageure car allier expressivité et efficacité est une tâche ardue. Les travaux exposés ici montrent comment l'utilisation de la programmation générative, et en particulier de la méta-programmation template, permet de répondre au problème de performances et d'abstractions.
Nous montrerons comment ces techniques ont permis de développer Quaff,
un outil de placement automatique d'applications data-flow sur des
cibles variées comme les clusters, les multi-coeurs ou le processeur
Cell.
Joel Falcou est maître de conférences en informatique au LRI,
Université de Paris 11. Ses travaux de thèse ont porté sur la
programmation parallèle pour la vision artificielle et plus
particulièrement sur les applications de la programmation générative
pour la création d'outils d'aide à la parallélisation. Il travaille
actuellement sur la définition de langages orientés domaine pour le
parallèlisme, outils qui s'intègrent dans divers projets de recherche
(ANR et System@tic).
http://www.lri.fr/~falcou
Mercredi 5 novembre 2008, 14h-17h, Amphi 2
Représentation efficace des données complexes dans un intergiciel schizophrène
- Documents
- quinot.ppt
Thomas Quinot, AdaCore
Dans un intergiciel schizophrène, une représentation intermédiaire des interactions entre composants applicatifs est construite et manipulée. Cette représentation est neutre vis-à-vis du choix d'une personnalité application (interface entre les composants et l'intergiciel) et d'une personnalité protocolaire (interface entre intergiciels distants). Elle rend possible le découplage entre ces deux aspects.
Cette représentation doit préserver la structure des données associées aux interactions. Cependant, sa construction in extenso s'avère coûteuse dans le cas de données composites complexes. Cette conversion peut être économisée en remplaçant la réplication complète de la structure par la définition d'un emballage « fantôme » autour de celle-ci (et de chacun de ses composants) : il suffit que cet emballage fournisse les accesseurs permettant de parcourir la structure et de construire un message la représentant.
Après avoir présenté un exemple concret de représentation neutre
des données structurées, nous montrons comment cette optimisation
peut être mise en oeuvre pour réaliser de manière efficace la
fonction de représentation dans un intergiciel schirophrène. Nous
concluons cette discussion par une évaluation du gain de performance
ainsi obtenu.
Thomas Quinot est docteur de l'Université Paris VI. Ses travaux de thèse
ont porté sur la définition d'une architecture d'intergiciel flexible
pour l'interopérabilité entre modèles de répartition. Il est aujourd'hui
Senior software engineer chez AdaCore, éditeur d'outils pour le
développement de systèmes embarqués, temps réel et critiques, où il
est notamment responsable des produits pour applications réparties.
http://www.adacore.com
Construire une application robuste sans faire exploser les coûts
- Documents
- tardieu.pdf
Samuel Tardieu, TELECOM ParisTech
Le langage Ada est connu pour sa sûreté intrinsèque : son typage fort, ses mécanismes de contrôle de valeurs et son système d'exceptions notamment permettent d'avoir une grande confiance en les programmes. Comme dit le vieux proverbe, « En Ada, quand ça compile, ça marche ».
Cependant, une des puissances d'Ada provient également de ses systèmes
de vérification lors de l'exécution du programme. Par exemple, si une
valeur se trouve en dehors de l'intervalle qui lui était autorisé, une
exception, rattrapable par le langage, sera automatiquement levée. Ce
système de vérification dynamique a bien évidemment un coût. Nous verrons
comment le système de compilation GNAT mélange analyse statique et
vérification lors de l'exécution pour fournir la totalité des
garanties définies par le langage tout en minimisant les surcoûts et
la perte de performance.
Samuel Tardieu est enseignant-chercheur à TELECOM ParisTech. Ses domaines
d'activité incluent notamment la compilation et la génération de code.
Il est également un des développeurs du système de compilation GCC,
et intervient plus particulièrement au niveau de GNAT, le compilateur
Ada de GCC.
http://www.rfc1149.net
Mercredi 26 novembre 2008, 14h-17h, Amphi 2
Mesure de Performance et Généricité à EDF R&D
- Documents
- plagne.pdf
Laurent Plagne ; EDF R&D Clamart.
L'outil BTL++ (Benchmark Template Library in C++) développé à EDF R&D se
fonde sur la programmation générique et permet de mesurer les performances
de noyaux de calcul intensif. Il s'agit d'une bibliothèque générique dont
la conception vise à faciliter l'extensibilité par l'utilisateur.
Récemment, le lien entre les mesures de performance et la génération
automatique de bibliothèques optimales à été étudié pour le domaine de
l'algèbre linéaire dense. Quelques mesures de performance de noyaux de
calcul à base d'"Expression Template" permettront d'illustrer l'usage de
l'outil BTL++.
Laurent Plagne est ingénieur-chercheur à EDF R&D où il conduit une mission d'expertise pour la conception des codes industriels de calcul intensif. Ses domaines de recherche principaux sont les solveurs parallèles pour équations aux dérivées partielles et la programmation générique appliquée au HPC.
Il est co-auteur d'une bibliothèque générique pour la mesure de
performance (BTL++) et est le développeur principal d'une bibliothèque
dédiées aux problèmes d'algèbre linéaire creux et structurés
(LEGOLAS++).
Bibliothèque générique multi-cible d'algèbre linéaire
- Documents
- kirschenmann.pdf
Wilfried Kirschenmann, EDF R&D
La multiplication des architectures HPC (CPU multi-coeurs, GPU, Cell,..)
implique autant de spécialisations des codes de calcul intensif. Dans un
contexte industriel, les codes de calcul multi-cibles posent alors des
problèmes de maintenance et d'évolutivité importants. La génération
automatique des spécialisations est une réponse à ces problématiques. Pour
le domaine de l'algèbre linéaire, nous étudions les possibilités offertes
par la programmation générique. La mise au point d'une bibliothèque
générique multi-cible et performante constitue le sujet de départ d'une
thèse dédiée aux méthodes de développement HPC qui minimisent l'adhérence
aux machines cibles.
Wilfried Kirschenmann est diplômé de l'école supérieure d'électricité. Il a
travaillé sur la parallélisation d'un solveur de neutronique sur processeur
graphique lors de son stage de fin d'étude à EDF R&D. Il va débuter une
thèse sur les méthodes de développement HPC qui minimisent l'adhérence aux
machines cibles.
Mercredi 11 février 2009, 14h-17h, P10
Programmer en JoCaml
- Documents
- maranget.pdf
- Keywords
- concurrency, language, caml, functional
Luc Maranget, Inria
JoCaml est une extension d'Objective Caml pour la programmation concurrente et distribuée, inspirée par le join-calcul. Nous avons récemment publié une nouvelle version de JoCaml, dont la compatibilité avec OCaml est meilleure que celle de la version initiale de F. Le Fessant. La nouvelle version pourra facilement être mise à jour au rythme d'OCaml et est binaire-compatible avec OCaml.
L'exposé s'attachera plus au langage JoCaml qu'au système JoCaml. Il montrera comment, à partir d'un programme potentiellement parallélisable écrit en OCaml (le ray tracer du concours ICFP 2001), on peut facilement produire un programme distribué, dans le cas abordé, très efficace. Ce sera l'occasion d'aborder la programmation en JoCaml de la coordination de multiples agents coopérants, d'une manière simple et concise dans l'esprit de la programmation fonctionnelle.
JoCaml est disponible en http://jocaml.inria.fr/.
Luc Maranget est chargé de recherche à l'Inria Rocquencourt. Il est
spécialiste de la conception et de l'implémentation des langages de
programmation, fonctionnels puis concurrents. À cet égard, il est
l'auteur du compilateur de filtrage d'Objective Caml et plus
récemment de la nouvelle version de JoCaml.
http://pauillac.inria.fr/~maranget/
ReactiveML : une extension d'OCaml pour la programmation de systèmes réactifs synchrones
- Documents
- mandel.pdf
Louis Mandel, Université Paris-Sud 11 - LRI
ReactiveML est une extension d'OCaml basée sur le modèle réactif synchrone introduit par F. Boussinot au début des années 90. Il permet la programmation de systèmes tels que les jeux vidéo ou les simulateurs.
Dans cet exposé, je présenterai ReactiveML à travers l'utilisation et
la programmation de rmltop, le pendant ReactiveML du toplevel
d'OCaml. Ce toplevel permet au programmeur d'écrire interactivement
des programmes ReactiveML qui sont typés, compilés et exécutés à la
volée. Toute expression ReactiveML valide peut être chargée dans le
toplevel et a la même sémantique et la même efficacité que sa version
compilée.
Louis Mandel est docteur de l'Université Paris 6. Il a passé un an
au laboratoire Verimag de Grenoble et un an à l'INRIA
Rocquencourt. Il est actuellement Maître de Conférences à
l'Université Paris-Sud 11. Il conçoit et développe ReactiveML.
http://www.lri.fr/~mandel
Mercredi 25 février 2009, 14h-17h, Amphi 1
Mise en oeuvre et application des extensions de langages
- Keywords
- language, concurrency
Patrick Viry, Ateji
Je présenterai sur la base d'une démo une application des extensions de langages, à savoir une extension Java pour l'optimisation. Cet exemple montre la mise en oeuvre concrète dans Eclipse, les gains de productivité et de qualité obtenus par rapport aux approches classiques Java+DSL, la différence entre cette approche et un générateur de code ou un préprocesseur. Il montre également une utilisation originale d'un compilateur: la génération automatique d'interface graphique.
Je parlerai aussi des futurs projets d'Ateji dans le domaine des
extensions de langage.
Patrick Viry a obtenu un doctorat d'informatique à l'INRIA-Lorraine en
1992. Il a poursuivi une carrière de chercheur à l'Université de
Kyoto, sur deux thèmes principaux: les modèles théoriques du
parallélisme et les outils de développement de type éditeur
syntaxique. Il a rejoint l'industrie en 1999, d'abord dans une société
japonaise réalisant des contrats pour le MITI, puis en tant
qu'architecte du langage OPL chez Ilog. Il a fondé Ateji en 2005 pour
développer et commercialiser des technologies innovantes dans le
domaine des langages et des outils de programmation.
www.ateji.com
Programmation par règles : application à la transformation d'arbres en Java
- Documents
- moreau-print.pdf, moreau-animated.pdf
- Keywords
- language, compilation
Pierre-Etienne Moreau - INRIA Nancy - Grand Est
Dans cet exposé je présenterai un outil, appelé Tom, qui permet de simplifier la programmation d'outils de manipulation et de transformation de structures arborescentes, telles que les AST (Abstract Syntax Trees) ou les documents XML par exemple. Tom est un langage de programmation qui ajoute à Java des constructions inspirées du calcul de réécriture et des langages à base de règles. On peut, de manière approximative, voir Tom comme une intégration d'un sous-ensemble de Caml dans Java.
Le langage repose sur trois notions fondamentales :
(i) les termes, qui sont un modèle universel permettant de décrire des structures arborescentes, et en particulier les notions de programmes et de preuves.
(ii) les règles, qui permettent de décrire de manière expressive des transformations.
(iii) les stratégies, qui permettent de contrôler l'application des règles.
La séparation transformation-contrôle est un point essentiel permettant de rendre les règles indépendantes de leur contexte d'utilisation, facilitant ainsi leur écriture, leur réutilisation et l'établissement de propriétés.
Le Langage Tom est parfaitement adapté à la réalisation d'outils de
transformation et de prouveurs. Son intégration dans Java rend son
utilisation facile, aussi bien dans le milieu académique que dans le
milieu industriel.
Pierre-Étienne Moreau est Chargé de Recherche à l'INRIA
Nancy-Grand Est, responsable de l'équipe Pareo. Il s'intéresse au
développement d'outils et de langages permettant de développer plus
rapidement des applications complexes et ceci de manière plus sûre.
Dans ce cadre, il a développé au cours de sa thèse le compilateur du
langage ELAN. Depuis 2001, il coordonne le développement de
l'environnement Tom, qui permet d'intégrer et d'utiliser les
notions de réécriture, de stratégie, de filtrage équationnel dans un
environnement de programmation Java. Les principales applications à ce
jour sont la réalisation de compilateurs, d'outils d'analyse et de
transformation de programmes, ainsi que des prouveurs automatiques.
http://tom.loria.fr, http://www.loria.fr/~moreau
Mercredi 25 mars 2009, 14h-15h30, Amphi 2
Que se cache-t-il derrière ce type ?
- Documents
- regis-gianas.pdf
Yann Régis-Gianas, laboratoire PPS (Univ. Paris Diderot), équipe πr² (INRIA)
Si une fonction φ promet de manipuler une valeur de type α sans l'observer, on peut utiliser son code sans risque pour toutes les affectations possibles de α : que la valeur soit entière (α = int) ou qu'elle soit un arbre (α = tree), la fonction se comportera toujours de façon identique. Cette propriété s'appelle le polymorphisme paramétrique, l'essence de la généricité.
Promettre de ne pas observer de trop près son argument est un fardeau parfois insupportable pour une fonction, pour des raisons algorithmiques (comment prendre une décision sans savoir ce que vaut mon argument ?), ou encore pour des raisons de performances de bas-niveau (si je sais que α = int, je peux utiliser une primitive dédiée de mon processeur). Même si le type d'une valeur est caché derrière un type plus abstrait α, on peut fournir des mécanismes pour « le redécouvrir » grâce à des tests dynamiques ou à des raisonnements purement statiques. La propriété qui permet de diriger son calcul par la forme des types est appelée le polymorphisme intentionnel.
Dans cet exposé, nous présenterons plusieurs versions du
polymorphisme intentionnel offertes par différents systèmes de types
et de preuves sûrs (c'est-à-dire garantissant que les programmes
ne peuvent pas planter et sont corrects vis-à-vis de leur spécification).
Yann Régis-Gianas est maître de conférence de l'Université Paris Diderot.
Ancien élève de l'EPITA et du LRDE (promo CSI 2003), il a poursuivi son
cursus par un DEA SPL (précurseur de l'actuel MPRI) et par un doctorat
au sein de l'équipe Gallium de l'INRIA. Il étudie le design des langages
de programmation à typage statique garantissant l'absence d'erreurs
dans les programmes.
http://www.pps.jussieu.fr/~yrg
Mercredi 22 avril 2009, 14h-17h, Amphi 2
Visite guidée de SmartEiffel: le génie logiciel en pratique.
- Documents
- colnet.pdf
Dominique Colnet. SmartEiffel - LORIA.
SmartEiffel, également connu sous le nom de GNU Eiffel, est à la fois un langage et un ensemble d'outils de compilations, de documentation et de validation.
Le langage SmartEiffel vise à favoriser la mise en pratique des principales exigences liées au développement d'un gros logiciel par une grande équipe. En plus d'exigences en terme de qualité, de sécurité et de documentation, la définition de SmartEiffel est également soucieuse de l'efficacité du programme à l'exécution. Ainsi, le modèle des objets qui est à la base du langage intègre également les types les plus élémentaires sans surcoût potentiel à l'exécution. Pour sa part, le mécanisme de programmation par contrats qui est essentiel en matière de documentation est également un bon moyen de rechercher les meilleures performances à l'exécution.
Durant cet exposé, la visite guidée du langage présentera le modèle
d'objets, la programmation par contrats, la double forme d'héritage
multiple ainsi que le mécanisme des agents.
Dominique Colnet, principal auteur de SmartEiffel, est membre du LORIA et
professeur d'informatique à l'IUT Nancy-Charlemagne.
http://SmartEiffel.loria.fr
Lisaac/IsaacOS: La puissance des langages objets à prototypes.
- Documents
- sonntag.pdf
Benoit Sonntag. ICPS - LSIIT.
Lisaac est un petit langage basé sur la technologie objet à base de prototype. Plus flexible que l'objet à base de classe, elle permet un dynamisme et un degré d'expressivité encore inégalés. Lisaac est inspiré du langage Self pour les concepts d'objets à prototypes et du langage Eiffel, pour les aspects d'ingénierie logicielle et notamment pour la programmation par contrat. Enfin, l'objectif étant de réaliser de la programmation de bas niveau à l'aide d'un langage de haut niveau, un ensemble de concepts utiles à la programmation système a été ajouté.
Le langage Lisaac utilise un nombre particulièrement restreint d'idiomes orthogonaux rendant difficile l'élaboration d'un compilateur efficace. Son compilateur en fait aujourd'hui l'unique langage à prototype compilé. Les performances atteintes sont proche des compilateurs C, voire même au-delà...
Pour étayer, approfondir et illustrer nos propos, nous ferons un rapide tour d'horizon du développement du système d'exploitation IsaacOS entièrement écrit en Lisaac.
Durant cet exposé, nous aborderons les thèmes suivants: concept à
prototype versus concept à classe; héritage multiple et dynamique et
autres particuliarité du Lisaac; technique de compilation et résultat
de performance; validation des concepts avec une brève présentation du
système d'exploitation IsaacOS.
Benoit Sonntag, principal auteur du projet Lisaac/IsaacOS, est membre
de l'équipe ICPS au LSIIT et Maître de conférence d'informatique à
l'UDS Strasbourg (Anciennement ULP).
http://isaacproject.u-strasbg.fr/
Mercredi 27 mai 2009, 14h-17h, P10
VMKit, LLVM et Clang: les prochaines générations de compilateurs
- Documents
- geoffray.pdf
Nicolas Geoffray, Lip6/INRIA/Regal
La Low-Level Virtual Machine (LLVM) est un ensemble de bibliothèques et d'outils qui facilitent le développement et l'optimisation de compilateurs, de générateurs de code et de machines virtuelles. Clang et VMKit utilisent LLVM pour leur générateur de code à différents niveaux: l'un pour la compilation statique de langages de la famille C (C/C++/ObjectiveC), et l'autre pour la compilation dynamique d'applications Java ou .Net.
Dans cet exposé, je présenterai ces trois projets, et rentrerai dans
les détails de VMKit, que j'ai développée dans le cadre de ma
thèse. Je finirai par montrer les exemples de recherche auxquels
nous nous adressons avec l'aide de VMKit, au sein de l'équipe de
recherche INRIA/Regal.
Nicolas Geoffray est doctorant à l'université Pierre et Marie Curie
dans l'équipe mixte Lip6/INRIA Regal. Sa thèse porte sur les machines
virtuelles applicatives et la manière dont elles sont utilisées dans
les projets de recherche. La soutenance est prévue à la fin de l'année
universitaire 2009.
http://pagesperso-systeme.lip6.fr/Nicolas.Geoffray/, http://vmkit.llvm.org, http://llvm.org, http://clang.llvm.org, http://vmkit.llvm.org, http://regal.lip6.fr
AutoVM: repousser les frontières de la généricité
- Documents
- thomas.pdf
Gaël Thomas, REGAL/Lip6/Inria
Avec l'avènement du Web et des applications réparties, les machines virtuelles applicatives sont devenues le support d'exécution de choix pour la plupart des applications. Développer et optimiser une machine virtuelle est un travail long et difficile qui requiert plusieurs années. Il s'avère que la plupart des machines virtuelles possèdent des composants communs: compilateur à la volée, ramasse-miettes, vérifieur de type, gestionnaire de threads, gestionnaire d'entrées/sorties, éditeur de liens paresseux, chargeur dynamique de code.
AutoVM est une machine virtuelle générique qui factorise ces composants communs et facilite le développement de nouvelles machines virtuelles, ou l'amélioration de machines virtuelles existantes.
Dans cet exposé, je présenterai l'architecture logicielle de notre
prototype AutoVM et montrerai sa généricité et son extensibilité.
Gaël Thomas est maître de conférences à l'université Pierre et Marie
Curie dans l'équipe mixte Regal/Lip6/Inria depuis trois ans. Ses
travaux de recherche portent sur la gestion des ressources,
l'isolation et la gestion de la concurrence dans les machines
virtuelles.
http://pagesperso-systeme.lip6.fr/Gael.Thomas/
Mercredi 30 septembre 2009, 14h-15h30, Amphi 4
GpuCV: Accélération par processeur graphique pour le traitement d'image et la vision artificielle
- Documents
- allusse_horain.pdf
Yannick Allusse et Patrick Horain
Nous décrirons brièvement l'état de l'art de l'utilisation des processeurs graphiques grand public (GPU) pour accélérer le traitement d'image, et nous en discuterons les limites. Puis, nous décrirons GpuCV, une bibliothèque logicielle libre et multi-plateforme pour accélérer par GPU les opérateurs de traitement d'image et de vision artificielle. GpuCV a été conçue pour être compatible avec la bibliothèque OpenCV et permettre d'intégrer facilement des opérateurs accélérés sur GPU dans des applications développées sur CPU. L'environnement GpuCV gère de façon transparente les caractéristiques du matériel, la synchronisation des données, l'activation à bas niveau des procédures GLSL ou CUDA, l'étalonnage et l'aiguillage vers la mise en oeuvre la plus performante et finalement offre un ensemble d'opérateurs de traiement accélérés par GPU.
Yannick Allusse est diplômé de l'ISTIA (2005). De 2005 à 2008, il a été ingénieur de recherche à Télécom SudParis et a été le principal développeur de la bibliothèque GpuCV. Ses domaines d'intérêt englobent l'infographie, la réalité virtuelle et le calcul intensif. Il est à présent consultant indépendant en optimisation logicielle.
Patrick Horain est Docteur-Ingénieur de l'INPG (1984) et enseignant-chercheur à l'Institut Télécom (ex GET) depuis 1986, d'abord à l'ENST puis à l'INT et Télécom SudParis. Ses recherches portent en particulier sur la vision 3D par ordinateur, en particulier pour la perception des personnes pour des applications interactives en réalité virtuelle, et sa mise en oeuvre en temps réel.
http://picoforge.int-evry.fr/projects/gpucv, http://www.viadeo.com/fr/profile/yannick.allusse, http://www-public.it-sudparis.eu/~horain
Mercredi 21 octobre 2009, 14h-16h, Amphi 4
CImg et G'MIC : Boites à outils libres pour le traitement d'images à différents niveaux
- Documents
- tschumperle.pdf
David Tschumperlé, GREYC Uni Caen.
Malgré la grande variété des types de données que l'on rencontre dans
le domaine du traitement d'images (1D,2D,3D, scalaires, couleurs,
multi-spectrales, séquences, etc...), nous sommes souvent amenés à
appliquer des algorithmes très classiques, ou des variations de ces
algorithmes, pour le pré-traitement, l'analyse ou la visualisation de
ces données images. Par conséquent, les logiciels et les bibliothèques
que nous utilisons dans notre recherche quotidienne, devraient
également être génériques, afin de s'adapter le mieux possible aux
données à traiter. Dans ce séminaire, je présenterai quelques outils
développés dans cette optique (au laboratoire GREYC, équipe IMAGE),
qui possèdent différents niveaux d'utilisations. Je commencerai tout
d'abord par présenter CImg, une bibliothèque C++ "template" (donc
générique par nature), qui a pour but de faciliter l'implémentation
d'algorithmes de traitements d'images personnalisés. Puis,
j'introduirais G'MIC, un langage de script reprenant la plupart des
éléments de CImg, qui est dédié au traitement et à l'analyse d'images
"de tous les jours". J'essaierai de montrer comment ces différents
outils indépendants sont organisés et comment ils cherchent à aider le
chercheur ou le programmeur en traitement d'images, autant d'un point
de vue programmation pure que d'un point de vue plus haut niveau.
David Tschumperlé est chargé de recherche CNRS, travaillant dans
l'équipe IMAGE du GREYC, depuis 2004. Il s'intéresse principalement
aux méthodes variationnelles et EDP pour le traitement d'images local
et/ou non-local.
http://www.greyc.ensicaen.fr/~dtschump/, http://cimg.sourceforge.net/, http://gmic.sourceforge.net/
Mercredi 2 décembre 2009, 14h-16h30, Amphi 4
Le processeur CELL : architecture et programmation
- Documents
- lamotte.pdf
Jean-Luc Lamotte
Le processeur CELL BE développé par le consortium IBM, Sony et Toshiba
a eu un impact important dans le monde du calcul scientifique mais
aussi dans le monde du jeu. Il est le processeur de base de la
première machine à avoir atteint 1 Pflops et aussi celui de la Play
Station 3 de Sony. Pour arriver à ce niveau de performance, il intègre
9 coeurs hétérogènes interconnectés par un bus. Le coeur principal
(PPE) appartient à la famille des PowerPC. Les 8 autres coeurs (SPE)
sont spécialisés pour le calcul. Après une présentation détaillée de
l'architecture du processeur, nous développerons son mode de la
programmation : lancement de threads de calcul sur les SPE, échange de
données, programmation SIMD.
Jean-Luc Lamotte est professeur à l'université P. et M. Curie
(UPMC). Ses travaux de recherche au sein du laboratoire d'informatique
de Paris 6 (LIP6) dans l'équipe PEQUAN (PErformance et QUalité des
Algorithmes Numériques) du département CALSCI (calcul scientifique)
portent sur le calcul haute performance en intégrant la vitesse de
calcul, mais aussi la qualité numérique des résultats obtenus. Il
enseigne notamment le parallélisme dans la spécialité SAR du master
d'informatique de l'UPMC.
http://www-pequan.lip6.fr/~lamotte/
La méthode multipôle rapide sur le processeur Cell : calcul du champ proche
- Documents
- fortin.pdf
Pierre Fortin
La méthode multipôle rapide (Fast Multipole Method, FMM) permet de
résoudre en temps linéaire le problème à N-corps, en astrophysique ou
en dynamique moléculaire par exemple. Nous présentons ici
l'implémentation sur le processeur Cell du calcul du champ proche de
la FMM, ce qui constitue un premier pas vers une implémentation
complète de la FMM sur ce processeur. Nous détaillerons les problèmes
rencontrés, au niveau de l'architecture comme au niveau de
l'algorithmique, ainsi que les diverses optimisations mises en
place. Notre implémentation permet de calculer jusqu'à 8,5 milliards
d'interactions par seconde (115,8 Gflop/s) sur un processeur Cell, et
jusqu'à 17 milliards d'interactions par seconde sur un IBM QS20 (230,4
Gflop/s), pour des distributions uniformes ou non uniformes de
particules.
Pierre Fortin est maître de conférences à l'Université Pierre et Marie
Curie dans l'équipe PEQUAN (LIP6) depuis deux ans. Ses travaux de
recherche portent sur le calcul scientifique parallèle haute
performance et sur les simulations numériques pour le problème à
N-corps. Depuis septembre 2009, il est responsable de l'option
"Calcul Intensif sur Nouvelles Architectures Parallèles" à
Polytech'Paris-UPMC.
http://www-pequan.lip6.fr/~fortin/
Mercredi 3 mars 2010, 14h-15h, Amphi 4
Yayi : Bibliothèque générique de traitement morphologique d'images
- Documents
- enficiaud.pdf
Raffi Enficiaud
Dans cet exposé, nous présenterons Yayi, une bibliothèque générique de
traitement morphologique d'image. Cette base logicielle, écrite en C++
et interfacée avec Python, fournit un nombre croissant de fonctions en
traitement d'image et en morphologie mathématique (distance,
segmentation, etc.). Nous discuterons de la mise en oeuvre générale,
des concepts génériques utilisés dans la bibliothèque, et de leurs
utilisations dans l'élaboration de nouveaux algorithmes. Enfin, nous
présenterons quelques pistes actuellement en développement dans Yayi
pour adresser certains des problèmes levés par la programmation
générique.
Raffi Enficiaud a soutenu sa thèse au Centre de Morphologie
Mathématique en 2007. Pendant sa thèse, il a participé au design et au
développement de Morph-M (anciennement Morphée) qui est une base
logicielle orientée recherche pour le traitement d'images et la
morphologie mathématique. Il s'est particulièrement intéressé à
l'extension multidimensionnelle et multispectrale des algorithmes
morphologiques, et a proposé de nouvelles méthodes de segmentation et
d'utilisation de la couleur. Après sa thèse, il travaillé à DxO sur le
thème de la quantification de défaut optique et capteur. Il travaille
depuis 2008 à l'INRIA Paris-Rocquencourt, équipe-projet IMEDIA en
qualité d'ingénieur expert, où il s'intéresse à l'indexation d'image
ainsi qu'à la visualisation de bases de donnée multimédia. Il
développe Yayi sur son temps libre.
http://raffi.enficiaud.free.fr/
Mercredi 31 mars 2010, 14h-16h, Amphi 4
Généricité en traitement d'images: niveau algorithmique et logiciel
- Documents
- fasquel.pdf
Jean-Baptiste Fasquel
Ce séminaire porte sur certains de mes travaux en matière de
généricité et réutilisation en traitement d'images. Ces travaux sont
présentés à une échelle algorithmique, bas-niveau, et à une échelle
logicielle, plutôt haut-niveau. À l'échelle de l'algorithme, nous
présentons une technique permettant d'étendre la généricité des
algorithmes de traitement d'images par rapport à la région d'intérêt
traitée, en complément de la généricité par rapport aux données
(1D, 2D, 3D, scalaires, couleurs, multi-spectrales, séquences,
etc.) Cette méthode repose sur une adaptation du patron de
conception « Iterator » et sur le polymorphisme de compilation en
C++. Au niveau logiciel, l'objectif de la généricité et de
réutilisation est de faciliter le couplage des algorithmes « purs »
avec des fonctionnalités supplémentaires telles que la visualisation,
l'interface homme-machine, les entrées-sorties... Dans ce cas, je
présente les principes d'une architecture flexible et évolutive
implémentée en C++, combinant la notion de (programmation par) rôle et
la notion de (programmation par) composants réutilisables. Ces travaux
sont illustrés par des applications dans le domaine médical.
Titulaire d'un diplôme d'ingénieur et d'un doctorat de l'université de
Strasbourg, Jean-Baptiste Fasquel a été, de 2002 à Septembre 2009,
chargé de recherche au sein de l'équipe informatique de l'IRCAD
(Institut de Recherche contre les Cancers de l'Appareil Digestif,
Strasbourg). Depuis Septembre 2009, il est enseignant-chercheur à
l'université d'Angers, rattaché au Laboratoire d'Ingénierie des
Systèmes Automatisés (LISA). Sa thématique de recherche concerne le
traitement des images, et couvre aussi bien l'aspect méthode que
l'aspect implémentation. Son domaine d'application principal est
l'aide au diagnostic médical.
http://www.istia.univ-angers.fr/LISA/PERSO/persoen.php4?nom=FASQUEL
Généricité et héritage en Eiffel
- Documents
- meyer.pdf
Bertrand Meyer
L'une des caractéristiques de la programmation objet est l'intégration
(introduite par Eiffel dans un article de la première conférence OOPSLA en
1986) entre les mécanismes d'héritage, permettant de structurer clairement
la description des systèmes, et de généricité, permettant le paramétrage de
ces descriptions. La combinaison de ces deux techniques d'architecture est
la clé de l'extensibilité et de la réutilisabilité permises par la
technologie objets. L'exposé montrera l'interaction entre la généricité et
l'héritage en Eiffel et l'application de ces concepts aux tâches d'analyse,
de conception et d'implémentation en génie logiciel. De nombreux exemples
illustreront l'application de ces idées, et compareront avec les solutions
adoptées dans des langages tels que Java et C\#.
Bertrand Meyer est professeur de génie logiciel à l'École Polytechnique
Fédérale de Zurich (ETH) et Chief Architect d'Eiffel Software (Santa
Barbara). Il est l'auteur de nombreux livres de génie logiciel et de
programmation par objets, en particulier "Object-Oriented Software
Construction") (version française chez Eyrolles, "Conception et
Programmation par Objets"), Jolt Award 1998 ; "Eiffel: Le Langage",
"Introduction à la Théorie des Langages de Programmation" (traductions
françaises chez InterEditions) ; et, récemment, "Touch of Class:
Introduction to Programming Well Using Objects and Contracts", un livre
d'initiation à la programmation (Springer). Il a reçu le System Award de
l'ACM pour son travail sur Eiffel et est membre de l'Académie des
Technologies.
http://se.ethz.ch/~meyer/
Mercredi 28 avril 2010, 14h-16h, Amphi Masters
Diagrammes de Décision à la Demande (DDoD)
- Documents
- linard.pdf
Alban Linard
Les Diagrammes de Décision (DDs) forment une vaste famille de structures de données, qui permettent de représenter et manipuler très efficacement de grandes quantités d'informations. Cependant, parmi les nombreux types de DDs, l'utilisateur est souvent désemparé pour choisir le bon. Souvent, aucun type ne répondant exactement à ce qu'il cherche, l'utilisateur doit faire adapter ses données au type de DDs choisi.
Le problème est que chaque type de DDs possède sa propre définition. Il n'existe aucun socle commun qui permette de définir n'importe quel type de DD. Ce problème se reflète au niveau des opérations manipulant les DDs. Celles-ci sont aussi spécifiques à chaque type.
Cet exposé présente les Polymorphic Decision Diagrams, un cadre assez
général permettant de spécifier de nombreux types de DDs
existants. L'utilisateur peut ainsi décrire simplement les DDs
correspondant le mieux aux données qu'il souhaite représenter. Ce
cadre permet de plus d'ajouter dans la spécification les informations
qui permettront de retrouver les performances des types définis
jusqu'à présent. Un exemple concret impliquant des loutres permettra
de montrer les possibilités offertes par ce cadre.
Alban Linard est post-doctorant à l'université de Genève, dans
l'équipe "Software Modeling and Verification". Sa thèse s'est déroulée
conjointement au LIP6, dans l'équipe Modélisation et Vérification et
au LRDE. Il s'intéresse aux Diagrammes de Décision et à leur
application dans le model checking.
http://smv.unige.ch
Architecture logicielle pour des outils génériques en traitement d'images
- Documents
- levillain.pdf
Roland Levillain
La plupart des frameworks de traitement d'images ne sont pas assez
génériques pour garantir une réutilisabilité effective des structures
de données et des algorithmes, tout en préservant performances et
facilité d'utilisation, et en restant proche de la théorie. Dans
cette présentation, nous proposons un cadre logiciel pour le
traitement d'images centré sur le paradigme de programmation
générique, cherchant à répondre tant aux besoins pratiques que
théoriques des scientifiques et des développeurs : la mise au point de
méthodes rapides et réutilisables, un niveau de généricité progressif,
la possibilité de traiter des ensembles de données volumineux, une
gestion de la mémoire automatique et efficace, la vérification
statique des types, l'orthogonalité des structures de données et des
algorithmes, etc. Cette approche permet aux utilisateurs de concevoir
et d'implémenter de nouvelles méthodes délivrées des contraintes
habituellement imposées pas les outils logiciels, de pratiquer des
expériences inter-domaines, de généraliser certains résultats et de
transformer facilement des prototypes en de vraies applications.
Roland Levillain est diplômé de l'EPITA (2003) et titulaire d'un
Mastère Spécialisé en Signal, Image et Reconnaissance des Formes
(SIRF) de l'ENST (2004). Depuis 2005, il travaille à l'EPITA et au
Laboratoire de Recherche et Développement de l'EPITA (LRDE) en tant
qu'enseignant-chercheur. Ses travaux portent sur le génie logiciel en
traitement d'images. Il participe au développement du projet Olena,
une plate-forme générique et performante pour le traitement d'images,
et poursuit une thèse sur le sujet depuis 2007.
http://www.lrde.epita.fr/cgi-bin/twiki/view/Main/RolandLevillain
Mercredi 2 juin 2010, 14h-16h, Amphi 4
Généricité et topologie discrète en C++
- Documents
- lamy.pdf
Julien Lamy
Le traitement d'images est par nature un procédé discret, au cours duquel un signal continu est décomposé en un ensemble de pixels, ou de voxels pour des images tri-dimensionnelles. Au niveau géométrique, cette nature discrète pose peu de problèmes, car la plupart des opérations géométriques sont indépendantes de la grille sous-jacente ; au niveau topologique, le problème est tout autre. Deux des notions fondamentales de la topologie, le voisinage et la connexité, sont radicalement différentes entre un espace continu et un espace discret : il est entre autres impossible de subdiviser un voisinage discret de façon infinie comme c'est le cas dans un espace euclidien.
Bien que certaines bibliothèques de traitement d'images contiennent des algorithmes topologiques, notamment de squelettisation, le type de voisinage utilisé par ces algorithmes est généralement fixé par le code, ce qui empêche une adaptation facile à un autre type de connexité ou à un espace de dimension différente.
Ce séminaire présente une méthode générique pour intégrer les notions
discrètes de voisinage et de connexité à une bibliothèque de traitement
d'images programmée en C++. Je montrerai également comment obtenir de
façon simple un algorithme de squelettisation homotopique en utilisant
ces notions.
Julien Lamy est titulaire d'un doctorat de l'Université de Strasbourg.
De 2001 à 2006, il a travaillé au sein de l'équipe de R&D de l'IRCAD
(Institut de recherche contre les cancers de l'appareil digestif,
Strasbourg) au développement d'algorithmes de traitement d'images
médicales. Depuis 2008, il est ingénieur de recherche au Laboratoire
d'imagerie et de neurosciences cognitives de l'Université de Strasbourg.
http://www-ulpmed.u-strasbg.fr/ipb/
Interface générique pour la parallélisation d'applications de recherche en imagerie biomédicale
- Documents
- cointepas.pdf
Yann Cointepas
Le projet BrainVISA (http://brainvisa.info) est en train de
développer, avec le soutien du projet européen HiPiP
(http://hipip.eu), une architecture générique pour la parallélisation
des applications. Cette architecture fournira un accès à divers moyens
de calculs (fermes de stations de travail, clusters, centres de
calculs, etc.) en s'appuyant sur des solutions existantes pour la
gestion des ressources (Sun Grid Engine, Condor, LSF, etc.) Cette
architecture est développée pour répondre aux besoins croissants de
moyens de calcul dans le monde de la recherche en neuroimagerie.
Au cours de ce séminaire, j'aborderai rapidement le contexte de la
recherche en neuroimagerie en me focalisant sur les besoins en
parallélisation d'applications. Ensuite, je détaillerai la solution
que nous avons choisie pour répondre à ces besoins.
Yann Cointepas a obtenu un doctorat de Traitement du signal et des
images à l'Ecole Nationale des Télécommunications de Paris en
1999. Depuis 2003, il a un poste d'ingénieur-chercheur à la Direction
des Sciences du Vivant du CEA. Il travaille au sein du laboratoire
LNAO situé à NeuroSpin. Il fait également partie des personnels de
l'IFR 49. Il est un des architectes historiques du projet
BrainVISA. Ses activités de recherche concernent principalement
l'analyse structurelle du cerveau humain avec de l'imagerie par
résonance magnétique (IRM) et plus particulièrement l'étude de la
connectivité cérébrale à partir d'IRM de diffusion.
http://www.lnao.fr/
Mercredi 13 octobre 2010, 14h-16h, Amphi 4
Recherche d'images et indexation multimédia basées contenu
- Documents
- picard.pdf
David Picard
Dans la recherche multimédia basée contenu, on distingue trois champs d'applications différents : la recherche de cible dans laquelle on désire retrouver un document particulier ; la recherche interactive, dans laquelle l'utilisateur définit l'objet de la requête au fil de son interaction avec le système ; et la catégorisation, où il s'agit d'étiqueter les données en un certain nombre de classes prédéfinies.
Cette présentation fera le tour d'horizon de mes travaux de recherche dans deux de ces domaines. Une première partie concernera la recherche de cible, où je présenterai le cas particulier de la recherche de quasi-copies dans de très grands volumes de données, et en particulier une application à la recherche de scènes urbaines identiques dans le cadre du projet iTowns.
Dans la deuxième partie, je développerai mes travaux récents sur la classification d'images. L'accent y sera mis sur la fusion de descripteurs multimédias et les techniques d'apprentissage statistique permettant d'apprendre conjointement l'opération de fusion avec la fonction de classification.
David Picard est actuellement maître de conférences à l'ENSEA (Cergy-Pontoise) au sein du laboratoire ETIS. Ses travaux de recherche sont centrés sur la reconnaissance de forme, l'apprentissage statistique ainsi que l'indexation de documents multimédia et la recherche d'information dans un contexte distribué. Il a obtenu sa thèse en 2008 sur la recherche d'image basée contenu à l'aide d'un système multi-agents, dans le cadre de données distribuées sur un réseau. Il a effectué ensuite un stage post-doctoral au LIP6 de l'université Pierre et Marie Curie, financé par le projet iTowns en partenariat avec l'IGN, pour la conception d'un moteur de recherche multimédia dans un contexte à la StreetView des rues de Paris.
Mercredi 10 novembre 2010, 14h-16h30, Amphi 4
Programmation par propriétés : application au traitement d'images
Vincent Tariel
L'idée d'une fonction est que la quantité d'entrée détermine complètement la quantité de sortie. En informatique, la quantité est une structure de données qui peut être simple, booléenne, entière, ou complexe, image, graphe, arbre. Dans ce domaine, un champ de recherche est de construire un ensemble de fonctions élémentaires, puis par composition d'en créer des plus compliquées. Pour cette dernière, une solution pratique est le langage Caméléon conçu par V. Tariel et O. Cugnon de Sevricourt, qui est un langage de flux de données génériques dont la sortie est prévue en janvier 2011. Générique signifie que tous les types de données peuvent être intégrés dans le langage. Pour cette première, ce séminaire couvrira quelques définitions de fonctions primaires reliées à l'image, incorporées à la bibliothèque standard de Caméléon. A la manière de l'implémentation de la bibliothèque standard du C++, il y aura l'utilisation d'un côté de l'algorithme générique for\_each en typage statique et de l'autre des opérateurs et des itérateurs organisés en programmation orientée objet. L'itérateur localise l'action suivant différents paradigmes : ensemble fini et dénombrable, voisinage, convolution, zone d'influence. L'opérateur agit suivant différents paradigmes : arithmétique, croissance de régions.
Ayant d'un côté un profile "informatique", ingénieur ESIEE avec un master en traitement d'images, et de l'autre côté un profile "science des matériaux", thèse en physique à l'école polytechnique avec un autre master en science des matériaux, le domaine de recherche de Vincent Tariel est axé sur l'image aussi bien expérimentalement, préparation de l'échantillon, microscopie, que numériquement, segmentation, caractérisation géométrique et physique, modélisation.
Il est rattaché au Department of Applied Mathematics, Australian National University
Mercredi 8 décembre 2010, 14h-16h30, Amphi 4
PHP.Reboot: un language de script utilisant la JSR 292
- Documents
- forax.pdf
Rémi Forax
Depuis 2000, on assiste à un regain d'intérêt pour les langages typés dynamiquement regroupés sous la bannière "langage de script". Pour les langages de script les plus populaires, comme PHP, Python ou Ruby, il existe, en plus des implantations écrites en C, des implantations plus récentes utilisant des environnements comme la machine virtuelle Java (JVM) ou la plateforme .Net. Ces implantations sont souvent plus efficaces que les implantations historiques, pourtant, ces environnements d'exécution utilisent des langages intermédiaires typés statiquement qui sont peu propices à l'implantation de langage typé dynamiquement. Partant de ce constat, le Java Community Process a créé la JSR 292 intitulée "Supporting Dynamically Typed Languages on the JavaTM Platform" dont le but est de proposer une API facilitant l'implantation et les performances des langages de script sur une machine virtuelle Java.
Mon exposé se compose de deux parties.
Dans un premier temps, en tant que membre du groupe d'experts, j'essaierai de restituer de façon didactique les concepts introduits par la JSR 292 en expliquant les tenants et les aboutissants.
La seconde partie, plus personnelle, montrera comment développer l'environnement
d'exécution d'un langage de script en utilisant les outils fournis par la JSR 292.
Je m'appuierai pour cela sur un prototype de langage que j'ai développé et nommé
PHP.reboot.
Rémi Forax est, depuis 2003, maître de conférence à l'université Paris Est Marne-la-Vallée
au sein du Laboratoire Informatique Gaspard Monge (LIGM). Ses travaux de recherche
sont centrés sur la conception de compilateurs et d'environnements d'exécution basée
sur des machines virtuelles.
Mercredi 9 février 2011, 14h-16h, Amphi masters
Principes et Pratiques de la Programmation Concurrente en π-calcul
- Documents
- peschanski.pdf
Frédéric Peschanski
Nous étudions la problématique du mélange de paradigmes de programmation
variés plongés dans un environnement concurrent. Dans cette
perspective, nous poursuivons
un cheminement similaire à celui qui conduit du lambda-calcul aux
langages fonctionnels, mais
en prenant comme point de départ le π-calcul. Nous proposons la
machine abstraite des π-threads
dont la principale originalité est l’absence de pile d’exécution.
Cette caractéristique
permet de nous reposer dans nos implémentations sur des algorithmes
simples et naturellement
concurrents, notamment pour ce qui concerne l’ordonnancement et le
ramasse-miettes. Pour ce
dernier, nous proposons un algorithme permettant de récupérer très
simplement les cycles de
processus en interblocage et autres structures bloquantes.
Frédéric Peschanski est Maître de Conférences à l'Université Pierre
et Marie Curie. Il effectue ses recherches au sein du laboratoire
d'informatique de Paris 6, dans l'équipe APR (algo-prog). Il étudie
essentiellement les langages de programmation avec comme leitmotiv
la théorie mise en pratique (et vice-versa).
Mercredi 16 mars 2011, 14h-16h, Amphi masters
Généricité en traitement des images : développement d’algorithmes complexes et localisés au sein d’une image.
Benoît Vandame
La plupart des bibliothèques génériques en traitement d’images mettent l’accent sur la généricité, la mise en pipeline d’opérations basiques, mais peu mettent l’accent sur la sélection d’un sous-ensemble de pixels concerné par un algorithme. En pratique de nombreux algorithmes ne s’appliquent que sur un sous-ensemble simple (rectangle) ou complexe (forme contiguë quelconque) de pixels qui ne sont qu’une petite fraction d’une image. La création d’un masque précisant les pixels concernés ne semble pas une solution optimale (contrainte mémoire et calculatoire). Dans le cadre de développement d’algorithmes en traitement d’images et vidéos, le laboratoire Canon Research Centre France (localisé à Rennes) développe une bibliothèque générique de traitement d’images qui ajoute la notion de forme à toute manipulation basique ou complexe d’une image. Une « arithmétique » des formes permet une sélection précise de pixels et une exécution efficace d’algorithme complexe. Les motivations, la mise en œuvre de cette bibliothèque, les outils template utilisés seront présentés et illustrés d’exemples concrets.
Benoît Vandame a obtenu sa thèse (2004) en traitement d’images appliqué à de grands relevés astronomiques au sein de l’European Southern Observatory (ESO-Munich). Depuis 2007, il travaille au laboratoire Canon Research Centre France (CRF-Rennes). Ses travaux portent sur le computational imaging (super-resolution, light-field imaging). Fort de son expérience en traitement automatique de larges données, il participe activement à la création d’une bibliothèque générique de traitement d’images pour les développements réalisés au sein du laboratoire CRF.
Mercredi 18 mai 2011, 14h-16h, Amphi masters
Utilisation des distances tangentes pour la compensation de mouvement : Application au codec Theora
- Documents
- fabrizio.pdf
Jonathan Fabrizio
Pour encoder de manière efficace une séquence vidéo, la redondance
temporelle est souvent utilisée. Pour cela, le mouvement entre l'image
considérée et une image de référence est estimé. Cela permet de
générer une prédiction à partir de l'image de référence et seule la
différence entre la prédiction et l'image réelle est enregistrée. Pour
estimer ce mouvement, les codecs se contentent souvent de suivre
l'évolution spatiale de blocs dans l'image. Ils associent, pour chaque
bloc de l'image considérée, un bloc similaire dans un voisinage proche
dans l'image de référence. Nous présentons ici une méthode originale
pour réaliser cette prédiction par compensation de mouvement. Notre
méthode utilise les distances tangentes. Cela permet non seulement
d'estimer l'évolution de la position des blocs de l'image mais en
partie aussi l'évolution du bloc lui-même. Nos prédictions sont donc
de meilleure qualité. Utilisée dans l'encodage de séquences, on peut
espérer un gain de compression non négligeable. Pour valider
l'efficacité de la méthode, nous intégrons cette méthode dans le codec
Theora et mesurons son efficacité en comparant les résultats obtenus
avec notre méthode et ceux obtenus par une stratégie classique (le
block-matching).
Jonathan Fabrizio est enseignant-chercheur au LRDE depuis l'été
2009. Il travaille actuellement sur la localisation et l'extraction
automatique de texte dans les images.
Mercredi 15 juin 2011, 14h-17h, Amphi masters
Modèle basé-contexte pour l'annotation automatique du multimédia
Nicolas Ballas
Ces dernières années ont vu exploser le nombre de vidéos disponibles
sur internet. Pour permettre leur exploitation, il est nécessaire de
mettre en place des systèmes analysant automatiquement ces données
multimédia. De tels systèmes permettent notamment d'indexer
automatiquement des vidéos en fonction de leurs contenus. Durant
cette présentation, je m'intéresserai aux récentes avancées effectuées
dans ce domaine. Je présenterai des descripteurs vidéos, développés
dans le cadre de ma thèse, qui capturent le mouvement et l'apparence
d'une vidéo pour les résumer dans une courte signature. Ces
signatures peuvent être utilisées a posteriori pour détecter
différents évènements ou concepts dans les vidéos.
Nicolas Ballas effectue sa thèse entre le laboratoire LVIC du CEA/List
et le laboratoire CAOR de l'école des Mines de Paris. Il s'intéresse
principalement au problème de perception automatique à travers l'étude
d'algorithmes combinant vision par ordinateur et apprentissage
automatique.
http://www.kalisteo.fr/en/index.htm, http://caor.mines-paristech.fr/
Traitement d'images sur processeur graphique avec CUDA et C++
- Documents
- garrigues.pdf
Matthieu Garrigues
Conçus à l'origine pour le rendu 2D et 3D, les processeurs graphiques (GPU) peuvent aujourd'hui être considérés comme des processeurs génériques massivement parallèles. Mais ce parallélisme impose des contraintes sur les algorithmes implantés et les types de données utilisés. D'autre part, le bus de communication entre le processeur central (CPU) et le GPU peut être un goulot d'étranglement.
Ce séminaire débutera par un aperçu des avantages et inconvénients de
la programmation GPU, puis je présenterai l'implantation d'un
algorithme temps réel de suivi de points dans une vidéo. Je terminerai
par l’introduction de deux petites boîtes à outils : Cuimg et Dige.
Cuimg utilise C++ pour simplifier l'écriture d'algorithmes de
traitement d'images avec CUDA, tandis que Dige, basée sur le framework
Qt, permet le prototypage rapide d'interfaces graphiques.
Matthieu Garrigues est diplômé de la promotion CSI 2009 de
l'EPITA. Depuis, il s'intéresse au développement et l'implantation
d'applications de vision par ordinateur sur des architectures
parallèles. Il est actuellement ingénieur de recherche à l'unité
d'électronique et d'informatique de l'ENSTA.
http://uei.ensta-paristech.fr
Mercredi 6 juillet 2011, 14h-15h, Amphi masters
Un algorithme rapide pour le Compressive Sensing sur architectures parallèles
- Documents
- borghi.pdf
Alexandre Borghi
Dans ce séminaire je présenterai un algorithme de résolution approchée
pour le problème du Compressive Sensing basé sur la programmation convexe.
Cet algorithme a la particularité d'avoir été pensé dès sa conception pour
tirer partie des architectures matérielles modernes, ce qui permet une
implémentation efficace et rapide sur celles-ci. Bien qu'une résolution
approchée soit en pratique suffisante pour obtenir rapidement une solution
de très bonne qualité, une variante exacte très rapide sera aussi
présentée. Cette dernière n'est toutefois utilisable que sous certaines
conditions. Trois types d'architectures parallèles sont ici envisagées :
des processeurs multi-cœurs avec unités de calcul vectoriel, des
processeurs graphiques (GPU) et le processeur Cell.
Alexandre Borghi est diplômé de la promotion CSI 2007 de l'EPITA et
effectue actuellement sa thèse au LRI de l'Université Paris-SUD XI. Il
s'intéresse principalement à l'adaptation de l'algorithmique aux
architectures parallèles.
http://www.lri.fr
Mercredi 26 octobre 2011, 14h-15h30, Amphi masters
Pourquoi Javascript est-il aussi rapide/lent ?
- Documents
- Javascript-Perf.pdf
Nicolas Pierron
Comment Javascript, un langage dynamique, interprété et non typé, parvient à être aussi rapide ? Quelles sont les avancées qu'il reste à faire pour obtenir des performances identiques au langage C ?
Pour illustrer cette présentation, on s’intéressera à l’évolution du
navigateur Mozilla Firefox et aux différentes approches pour résoudre
ce problème.
Diplômé de la promotion CSI 2008 de l'EPITA, Nicolas Pierron travaille
actuellement à Mozilla Paris sur le nouveau moteur Javascript
IonMonkey.
http://www.mozilla-europe.org/fr/
Mercredi 16 novembre 2011, 14h-16h, Amphi A4
Interactive 2D and 3D Segmentation with ilastik
Ullrich Köthe
The ilastik system developed by our group uses machine learning and
simple interaction techniques to empower users without special image
processing expertise to segment and analyze their 2- and 3-dimensional
image data on their own. It offers a number of easy-to-use workflows
for various common analysis tasks. The talk will present two of these
workflows (“interactive classification” and “region carving”), going
from an online demonstration of the high-level user experience down to
the algorithmic and software design details. Special emphasis will be
put on aspects of genericity and parallelization which facilitate
convenient adaptation of basic building blocks to different contexts
without loss of performance. Examples from challenging biological
applications will illustrate our system's capabilities.
Ullrich Köthe is a senior researcher in the Multidimensional Image Processing Group at the Interdisciplinary Centre for Scientific Computing of the University of Heidelberg, Germany, where he heads advanced research on image and data analysis for industry and the life sciences. Formerly, he was with the Cognitive Systems Group at the University of Hamburg (1999-2007) and with the Fraunhofer-Institute for Computer Graphics in Rostock (1992-1999).
Ullrich Köthe's main field of research is the development of
user-friendly image analysis methods. He is interested in all
techniques that facilitate genericity and re-usability, from machine
learning and probabilistic modeling to generic programming and
empirical performance evaluation. Dr. Köthe is the originator and
maintainer of the open-source image analysis library VIGRA and
co-developer of the interactive ilastik toolkit, which have been
designed to put these ideas into practice.
http://www.ilastik.org
Mercredi 15 février 2012, 14h-17h, Salle Master
Des performances dans les nuages avec la virtualisation des langages
Yann Régis-Gianas
«The effective exploitation of his powers of abstraction must be regarded as one of the most vital activities of a competent programmer.» disait Dijsktra.
En effet, pour aborder la complexité d'un problème, l'explicitation des concepts utiles à sa formalisation et à sa résolution est bien souvent une étape clé. Lorsque que l'on étend ce processus à une classe de problèmes qui partagent les mêmes concepts, il est naturel de se doter d'un langage le plus approprié possible pour manipuler ces abstractions spécifiques à un domaine (en anglais, «Domain Specific Language»).
Comment implémenter ces DSLs? Une première approche classique reflète les constructions du DSL sous la forme d'un jeu de fonctions de bibliothèque. L'avantage de cette approche est d'utiliser directement son langage généraliste préféré, et sa chaîne de compilation optimisée, de façon à générer du code machine à moindre frais. Par contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques au DSL - à moins d'utiliser des techniques pointues de méta-programmation - est a priori impossible.
Une seconde approche, opposée, consiste à écrire un compilateur pour le DSL à partir de zéro. Toute liberté est alors donnée à l'implémenteur d'intégrer à son compilateur des passes d'optimisation spécifiques… mais au prix d'une réimplémentation de passes de compilation déjà présentes, et certainement plus abouties, dans le compilateur de son langage généraliste favori.
Dans cet exposé, je présenterai les travaux de Martin Odersky et
son équipe sur la virtualisation de DSLs à l'intérieur du langage de
programmation Scala. La virtualisation de langage utilise
intensivement le polymorphisme et la composition mixin de Scala ainsi
que des techniques de génération de code à l'exécution pour embarquer
des langages spécifiques dans Scala dont la compilation peut
réutiliser des modules du compilateur mais aussi étendre ces derniers
par des optimisations spécifiques au domaine.
Yann Régis-Gianas est un ancien élève de l'EPITA, promo CSI 2003. À sa
sortie de l'école, il a poursuivi un troisième cycle en passant un DEA
à l'Université Paris Diderot et une thèse à l'INRIA Rocquencourt. Il
est aujourd'hui maître de conférence à Paris Diderot et travaille sur
le design des langages de programmation et de preuve.
http://www.pps.jussieu.fr/~yrg/
Certification d'annotations de coût dans les compilateurs
- Documents
- ayache_EPITA.pdf
Nicolas Ayache
Nous traitons du problème de la conception d'un compilateur où des
informations sur le coût à l'exécution du code objet sont retournées
en tant qu'annotations de coût sur le code source, et ce de façon
certifiée correcte. Pour cela, nous avons besoin d'une idée souple et
précise : (i) du sens donné aux annotations de coût, (ii) de la
méthode pour les prouver correctes et précises, et (iii) de la manière
d'en composer les preuves. Nous proposons ce que nous appelons une
approche par étiquetage pour répondre à ces trois questions. Dans un
premier temps, nous montrons son application sur un compilateur jouet.
L'étude formelle qui en découle suggère que l'approche par étiquetage
a de bonnes propriétés de compositionnalité et de passage à l'échelle.
Afin de s'en convaincre davantage, nous rapportons notre retour
d'expérience sur l'implémentation d'un compilateur prototype écrit en
ocaml pour un large sous-ensemble du langage C.
Nicolas Ayache, ancien doctorant Université Paris-Sud / CEA-LIST, est
actuellement Post-doc au laboratoire PPS (Preuves, Programmes et
Systèmes) à l'université Paris Diderot.
Mercredi 14 mars 2012, 14h-16h, Amphi 3
Reusable Generic Look Ahead Multithreaded Cache - a case study for a high resolution player
- Documents
- chatelet.pdf
Guillaume Chatelet
L'industrie des effets spéciaux produit une grande quantité d'images
qu'il faut traiter et afficher. Dans le cadre de ses développements
internes, Mikros Image a développé et mis en Open Source un player
d'images temps réel : duke. Dans cet exposé je décrirai quels sont
les enjeux techniques d'un tel logiciel (allocation mémoire, accès
disque, multiplicité des formats, affichage, traitement...) puis
j'expliquerai plus en détails les étapes de la conception d'un
composant essentiel permettant de lire et décoder le plus rapidement
possible les images à afficher. Ce composant ayant pour but d'être
intégré dans d'autres outils, il doit être réutilisable.
Guillaume Chatelet est diplômé de l'ENSICaen et titulaire d'un DEA en
intelligence artificielle et algorithmique. Il travaille en qualité
d'ingénieur recherche et développement à Mikros Image depuis sept
ans. En 2007, il contribue à la bibliothèque Loki, initiée par Andrei
Alexandrescu, puis à la plate-forme Eclipse.
http://www.mikrosimage.eu/, https://github.com/mikrosimage/duke, https://github.com/mikrosimage/concurrent utils
Mercredi 21 mars 2012, 14h30-16h30, Amphi 3
Le point de vue d'un théoricien sur l'intérêt de la généricité pour le traitement d'images
- Documents
- najman.pdf
Laurent Najman
Une question fondamentale pour mes recherches est de savoir ce qu'est une image. Cela peut sembler à première vue une question trop simple : une image, c'est un ensemble de points. Mais ces points sont reliés entre eux, c'est ce qu'on appelle une structure, et ils ont des données de types multiples qui leur sont attachées. La bibliothèque Milena, développée au LRDE, est une bibliothèque générique dédiée au traitement d'images. Dans Milena, trois axes indépendants sont développés : l'axe des structures, l'axe des données, et celui des algorithmes, c'est-à-dire de ce qu'on peut faire avec une image.
Dans cet exposé, je vais développer plusieurs exemples dans lesquels je choisirai un algorithme et un type de données, en faisant varier la structure. Changer la structure, c'est penser les images d'une manière différente, et c'est quelque chose d'extrêmement porteur en recherche.
- Un premier exemple est celui d'un algorithme classique de
segmentation : la ligne de partage des eaux. Originellement pensé sur les pixels, sa traduction dans le cadre des arêtes donne le problème classique d'arbre couvrant de poids minimum. Si la ligne de partage des eaux est très connue en traitement d'images, les arbres de poids minimum sont très utilisés en classification. Un pont naturel est alors établi entre deux communautés différentes, et les idées provenant de ces deux communautés peuvent être combinées.
- Un deuxième exemple est celui de la représentation arborescente des
images. Pour illustrer, tant les lignes de niveaux que les composantes connexes des ensembles de niveaux (les coupes) des images sont naturellement structurées en arbre : deux lignes ou deux composantes sont soit disjointes soit emboîtées. On peut filtrer une image en éliminant de l'arbre tous les nœuds qui ne vérifient pas un critère. Mais on peut aussi considérer l'arbre lui-même comme une image, et appliquer sur cet arbre un algorithme de traitement d'images. C'est une idée récursive très riche.
D'autres exemples pourront être développés en fonction du temps : liens entre ligne de partage des eaux topologique et segmentation hiérarchique, topologie discrète dans divers cadres...
La bibliothèque Milena permet d’appliquer la plupart des algorithmes
existants à une nouvelle structure, ce qui est un gain de temps
incontestable. Cela permet de se concentrer sur ce qui fait le cœur
de mon métier: chercher un algorithme plus efficace, adapté à un type
de structure, ou encore chercher quelles sont les propriétés
mathématiques d’un algorithme sur une structure donnée.
Laurent Najman a reçu l’habilitation à diriger les recherches de l'université de la Marne-La-Vallée en 2006, un doctorat en mathématiques appliquées de l’université de Paris-Dauphine en 1994, et un diplôme d’ingénieur de l'École des Mines de Paris en 1991.
Il a travaillé chez Thomson-CSF sur la segmentation d'images infrarouges en utilisant la morphologie mathématique, chez Animation Science sur des systèmes de particules pour l'infographie et de la visualisation scientifique, puis chez OCÉ sur des problèmes d’analyse et de traitement d'images pour l'impression.
Depuis 2002, il est enseignant-chercheur à l’ESIEE, actuellement
professeur, membre du Laboratoire d’Informatique Gaspard-Monge
(Université Paris-Est). Ses recherches portent sur la morphologie
mathématique discrète et l’optimisation discrète.
Mercredi 9 mai 2012, 14h00-17h30, Amphi 3
Un modèle générique de traitement et de représentation des images
- Documents
- manzanera.pdf, manzanera.zip
Antoine Manzanera
Concilier généricité et performance des systèmes de vision a toujours été au cœur des préoccupations scientifiques du laboratoire d'Électronique et Informatique d'ENSTA-ParisTech. Nous y avons abordé ce problème sous différents points de vue: électronique, algorithmique, et logiciel. Depuis nos travaux sur les rétines programmables et leur algorithmique exotique, nous avons progressivement intégré la multiplicité des modèles et structures de données, ainsi que l'emprise des architectures sur étagères, pour appréhender l'hétérogénéité des systèmes multi-plateformes.
Dans cette présentation à deux voix, on abordera le problème sous deux angles complémentaires, l'un touchant au modèle et aux algorithmes, l'autre au logiciel et aux plateformes de calcul.
Ce premier exposé présente un modèle générique de traitement et de
représentation des images fondé sur les espaces de caractéristiques
"local jets" (LJ, ou dérivées partielles multi-échelles), comme
exemple de cadre algorithmique unifié. Grâce à un espace où la
métrique naturelle est directement liée à la similarité visuelle, ce
cadre permet d'aborder un grand nombre d'opérateurs de traitement
d'images de bas niveau, qui correspondent généralement à la
rétro-projection dans l'espace image de points de l'espace des
caractéristiques transformé. Il permet aussi d'aborder des
représentations visuelles de plus haut niveau (modèles d'objet par
exemple) à partir de statistiques globales extraites de l'espace des
caractéristiques. On justifiera cette représentation et on
l'illustrera par diverses applications : Moyennes non locales
(NL-Means) par Convolution dans l'espace LJ pour le débruitage de
vidéos, Calcul du flux optique par recherche du plus proche voisin
dans l'espace LJ, Modélisation de fond statique par échantillonnage de
l'espace LJ, Détection d'objets par transformée de Hough dense...
Antoine Manzanera est diplômé de l'Université Claude Bernard à Lyon
(Licence de Maths 1991 et Master d'Informatique Fondamentale 1993), et
Docteur de Télécom-ParisTech en Signal et Images ("Vision artificielle
rétinienne", 2000). Depuis 2001 il est Enseignant-Chercheur à
l'ENSTA-ParisTech. Dans ses recherches, il s'intéresse au Traitement
d'Images et à la Vision de bas niveau, du modèle mathématique à
l'implantation parallèle sur un système embarqué. Il enseigne
principalement en 2ème et 3ème année du cycle Ingénieur ENSTA, et dans
le Master d'Informatique de l'UMPC (Paris 6), dans les spécialités
Imagerie et IAD.
http://www.ensta-paristech.fr/~manzaner
Analyse des mouvements apparents dans un flux vidéo
- Documents
- garrigues.pdf
Matthieu Garrigues
Dans ce second exposé, Matthieu Garrigues parlera de ses travaux sur
l'analyse des mouvements apparents dans un flux vidéo. La primitive de
base, présentée dans un séminaire précédent, permet le suivi temps
réel (supérieur à 30 images par seconde) de plusieurs milliers de
particules. Ces travaux nous ont permis de développer un cadre
générique facilitant l'analyse de scènes dynamiques prises de caméras
fixes ou mobiles. Nous montrerons comment cette brique logicielle a
été utilisée dans deux exemples d'applications : l'extraction des
plans principaux et l'estimation de la profondeur dans un système
mono-caméra. Le suivi de particules a été implémenté sur processeurs
graphiques avec le framework CUDA, et sur CPU-multicœurs avec
OpenMP. Nous expliquerons comment C++ a été utilisé pour factoriser un
maximum de code entre ces deux implémentations.
Matthieu Garrigues est diplômé de la promotion CSI 2009 de
l'EPITA. Depuis, il s'intéresse au développement et à l'implantation
d'applications de vision sur des architectures parallèles. Il est
actuellement ingénieur de recherche à l'unité d'électronique et
d'informatique de l'ENSTA, où il travaille sur l'analyse temps réel de
scènes acquises par des systèmes mobiles mono-caméra.
http://www.ensta-paristech.fr/~garrigues
Mercredi 20 juin 2012, 14h00-16h00, Amphi 3
GPU Computing : début d'une ère ou fin d'une époque ?
- Documents
- mahe.pdf
Eric Mahé, responsable du projet OpenGPU
L'arrivée des GPU (Graphics Processing Unit) a profondément changé la manière de concevoir la notion de coprocesseur. A moins de 500€, il est désormais possible d'avoir à sa disposition une puissance de calcul qui n'était réservée jusqu'à un passé récent qu'aux grands centres de calcul. La société Nvidia, en mettant au point l'environnement CUDA, a fourni à la communauté des développeurs des moyens simples et efficaces pour rendre cette puissance de calcul accessible au plus grand nombre. Depuis, sous l'impulsion de la société Apple, le standard OpenCL est venu ouvrir la voie d'une véritable parallélisation des applications sur l'ensemble des ressources processeur offertes aux développeurs.
Cet exposé décrira les différentes technologies permettant la programmation
parallèle des GPU en mettant l'accent sur les contraintes actuelles et les
progrès à venir des futures architectures comme le processeur Kepler. Des
démonstrations ainsi que des exemples de code viendront compléter cet
exposé.
Eric Mahé a été responsable des nouvelles technologies au sein de l'équipe marketing de Sun France pendant 20 ans après avoir occupé différents postes de chef de projet dans le domaine du nucléaire et de la défense. Son rôle fut d'évangéliser les choix technologiques et stratégiques de Sun auprès des communautés concernées par le langage Java, les développements du Logiciel Libre et les applications citoyennes de la fédération d'identité basées sur le projet Liberty Alliance. Diplômé de plusieurs troisièmes cycles en marketing, biologie et informatique, Eric Mahé est administrateur de l'association Silicon Sentier, expert auprès du pôle de compétitivité CAP Digital et professeur de communication à l'université René Descartes – Paris V.
Eric Mahé assure depuis 2009 la direction du projet OpenGPU dont l'objectif
est la mise au point de nouvelles chaînes de compilation à destination des
architectures hybrides GPU/CPU et a fondé la société MassiveRand spécialisée
dans les nombres aléatoires dans le domaine de la sécurité.
Mercredi 4 juillet 2012, 14h00-16h30, Amphi 4
Vérification efficace de propriétés insensibles au bégaiement.
- Documents
- ben-salem.pdf
Ala Eddine Ben Salem (doctorant)
Le model checking est une technique de vérification formelle automatique. Prenant en entrée un modèle décrivant toutes les exécutions possibles du système et une propriété exprimée sous la forme d'une formule de logique temporelle, un algorithme de model checking répond si le modèle satisfait ou non la formule. Le problème principal du model-checking est l'explosion combinatoire de l'espace d'états décrivant le système.
Afin d'améliorer les performances, on a apporté les contributions suivantes
à l'approche automate du model checking. D'abord l'amélioration de
l'algorithme de vérification en deux passes de l'approche basée sur les
automates Testeur TA (Testing Automaton). Ensuite la proposition d'une
méthode permettant de transformer un automate TA en un automate vérifiable
en une seule passe, qu'on a appelé STA (Single-pass Testing
Automaton). Enfin, la contribution la plus significative est un nouveau type
d'automate baptisé TGTA (Transition-based Generalized Testing
Automaton). L'apport principal de cette nouvelle approche consiste à
proposer une méthode permettant de supprimer les transitions bégayantes dans
un TGTA sans avoir besoin, ni d'ajouter une seconde passe comme dans
l'approche TA, ni d'ajouter un état artificiel comme dans l'approche STA.
A.E. Ben Salem est ingénieur ENSEEIHT-2005 en Informatique et Mathématiques
Appliquées, il a obtenu en parallèle un Master Recherche Sûreté du Logiciel
et Calcul à haute Performance à l’INP Toulouse. Depuis 2011, il est
doctorant au LRDE et au LIP6 sur la vérification formelle de propriétés sur
des systèmes logiciels, en lien avec le projet Spot.
Composition dynamique de techniques pour le model checking efficace
- Documents
- renault.pdf
Étienne Renault (doctorant)
Le model checking est une technique qui permet de s'assurer qu'un système
vérifie un ensemble de caratéristiques appelées propriétés. Le système et la
négation de la formule sont ensuite représentés de manière abstraite (ici un
automate) pour pouvoir détecter des comportements incohérents. Ces
propriétés ont été classifiées et possèdent des particularités qui peuvent
être exploitées afin de réduire la complexité du processus de
vérification. Nous montrerons ici comment tirer parti dynamiquement des
différentes classes de formules.
E. Renault est diplômé de Paris VI en système et applications réparties, il
s'intéresse à la vérification formelle des systèmes concurents. Il a
intégré cette année le LRDE dans le cadre de sa thèse portant sur la
composition dynamique de techniques pour le model checking efficace. Ce
travail, en collaboration avec l'équipe MoVe du Lip6, s'intègre au projet
Spot.
Filtrage morphologique dans les espaces de formes : Applications avec la représentation d'image par arbres
- Documents
- xu.pdf
Yongchao Xu (doctorant)
(Morphological Filtering in Shape Spaces: Applications using Tree-Based Image Representations)
Connected operators are filtering tools that act by merging elementary
regions of an image. A popular strategy is based on tree-based image
representations: for example, one can compute a shape-based attribute on
each node of the tree and keep only the nodes for which the attribute is
sufficiently strong. This operation can be seen as a thresholding of the
tree, seen as a graph whose nodes are weighted by the attribute. Rather than
being satisfied with a mere thresholding, we propose to expand on this idea,
and to apply connected filters on this latest graph. Consequently, the
filtering is done not in the image space, but in the space of shapes built
from the image. Such a processing is a generalization of the existing
tree-based connected operators. Indeed, the framework includes classical
existing connected operators by attributes. It also allows us to propose a
class of novel connected operators from the leveling family, based on shape
attributes. Finally, we also propose a novel class of self-dual connected
operators that we call morphological shapings.
Yongchao Xu received the B.S. degree in optoelectronic engineering from
Huazhong University of Science and Technology, China, in 2008, the "diplôme
d'ingénieur" in electronic & embedded system at Polytech' Paris-Sud and the
M.S. degree in signal & image processing from Université Paris Sud, in 2010.
He is currently a PhD student at Université Paris Est working on image
segmentation, morphological image analysis and, especially shape-based
connected morphology.
Mercredi 17 octobre 2012, 10h00-12h00, Salle L-Alpha du LRDE
Systèmes d'exploitation en dur: une clef du passage de 10 à 1000 cœurs
- Documents
- poss.pdf
Raphael Poss - University of Amsterdam
Afin d'exploiter le potentiel des puces multi-cœurs pour une performance évolutive et à haut rendement énergétique, le projet Apple-CORE a co-conçu un modèle général d'architecture matérielle et une interface de contrôle de parallélisme. Cette interface, appelée SVP, est réalisée par du matériel sur puce dédié à la gestion de la concurrence de programmes parallèles exécutés sur plusieurs cœurs. SVP se base sur les principes de synchronisation de flux de données («data flow»), de programmation impérative et d'exécution efficace du parallélisme en termes de budget temps et énergie. Les composants matériels correspondants peuvent coordonner plusieurs cœurs RISC équipés de multi-threading matériel, organisés en clusters de calcul sur puce, dits «Microgrids».
Comparés à l'approche traditionnelle «accélérateurs», les Microgrids sont destinés à être utilisés comme composants dans les systèmes distribués sur puce contenant à la fois des grappes de petits cœurs et optionnellement de gros cœurs –optimisés pour l'exécution séquentielle– disponibles en tant que «services» pour les applications. Les principaux aspects de cette architecture sont l'asynchronisme, c'est-à-dire la capacité à tolérer les opérations irrégulières avec des temps de latence longs, un modèle de programmation à échelle invariante, une vision distribuée de la puce, et une mise à l'échelle transparente de la performance d'un seul code binaire à plusieurs tailles de grappes de cœurs.
Cette présentation décrit le modèle d'exécution, la micro-architecture des
cœurs, sa réalisation au sein d'une plateforme et son environnement
logiciel.
Diplômé CSI en 2003, Raphael est resté actif à l'EPITA jusqu'en 2004, puis a
travaillé en tant qu'ingénieur logiciel à Paris puis Rotterdam. Il rejoint
en 2008 le groupe Computer Systems Architecture à l'Université d'Amsterdam
en tant que chef de projet et enseignant-chercheur, où il reçoit un doctorat
en septembre 2012. Il donne des cours d'architecture matérielle à Amsterdam
et Leiden, et continue de coordonner des activités de recherche au
croisement entre architecture, compilateurs et systèmes d'exploitation.
http://staff.science.uva.nl/~poss
Platform and Research overview on the Intel Single-chip Cloud Computer
- Documents
- bakker.pdf
Roy Bakker - University of Amsterdam
The Single-chip Cloud Computer (SCC) is a 48-core experimental processor created by Intel Labs targeting the many-core research community. The 6x4 mesh Network-on-Chip provides 24 tiles with 2 cores each. All cores are independent and run their own instance of an operating system. It has hardware support (local buffers on the tiles) for sending short messages between cores, and allows for voltage and frequency control at 8 and 2 cores respectively.
We have already modified the SVP runtime system to use these on-chip buffers for the communication between threads executed on separate cores. We also created a visual application for manual process migration and scheduling on the SCC as well as a library for customized voltage and frequency scaling on the chip.
Currently we focus on automated parallelization and mapping of one or
multiple sequential programs onto the 48 cores by modifying the daedalus
framework to target the SCC. The daedalus framework parallelizes sequential
C programs using Kahn Process Networks (KPNs) and generates code to run the
KPN on multiple hardware platforms like for example an FPGA, SMP CPU or
GPU. The SCC backend, which is work in progress, should result in a tool
that utilizes the SCC cores in an optimal way by means of performance and
energy consumption. It should also allow the system to dynamically adapt on
changes in the computational or communicational needs of the processes by
scaling frequency and migrating processes.
Roy Bakker is a PhD student in the Computer Systems Architecture group at
the University of Amsterdam, where he also graduated for his Bachelor's
(2008) and Master's (2011) degree. His current work is funded by the
Netherlands Organisation for Scientific Research (NWO) project on Smart
Energy Systems (SES).
http://www.science.uva.nl/~bakkerr
Mercredi 23 janvier 2013, 11h-12h, Salle L-Alpha du LRDE
Amélioration du design et des performances des machines virtuelles langages
- Documents
- thomas.pdf
- Keywords
- languages, vm, java
Gaël Thomas - REGAL-LIP6/UPMC/INRIA
Avec l'avènement du Web et du besoin de protéger les utilisateurs contre des logiciels malicieux, les machines virtuelles langages, comme les machines virtuelles Java et .Net, sont devenues la norme pour exécuter des programmes. Dans cet exposé, je vais présenter les travaux que j'ai menés ces dernières années et qui se sont concentrés sur trois aspects des machines virtuelles: leur design, leur sûreté de fonctionnement, et leur performance sur les architectures multi-cœurs.
Ma première contribution est VMKit, une bibliothèque qui facilite le
développement de nouvelles machines virtuelles performantes en cachant leur
complexité dans un ensemble de composants réutilisables. Ma seconde
contribution est I-JVM, une machine virtuelle Java qui élimine les huit
vulnérabilités connues qu'un composant de la plateforme OSGi pouvait
exploiter. Ma troisième contribution vise à améliorer les performances des
machines virtuelles sur les architectures multi-cœurs en se focalisant sur
les verrous et les ramasse-miettes: avec un mécanisme de verrouillage qui
surpasse tous les autres mécanismes connus lorsque le nombre de cœurs
augmente, et avec avec une étude des goulets d'étranglement des
ramasse-miettes sur les architectures multi-cœurs.
Gaël Thomas est maître de conférences (HDR) à l'UPMC Paris Sorbonne qu'il a rejointe en 2006 après avoir passé une année en post doctorat à l'université Joseph Fourier. Il est membre de l'équipe REGAL du LIP6, une équipe mixte entre l'INRIA et l'UPMC qui étudie les systèmes d'exploitation et les systèmes distribués à large échelle. Ses travaux visent à améliorer les performances, la modularité et la sûreté de fonctionnement des machines virtuelles langages comme la machine virtuelle Java.
Depuis 2011, il est président de l'association ACM SIGOPS France.
http://pagesperso-systeme.lip6.fr/Gael.Thomas/
Mercredi 20 février 2013, 11-12h, Salle L-Alpha du LRDE
Une représentation d'images 2D discrète, continue et auto-duale
- Documents
- geraud.pdf, images.zip, chambery-geometry-2008-slides.pdf
Thierry Géraud, EPITA-LRDE
En morphologie mathématique, la représentation d'une image par l'arbre
des formes n'est en fait pas vraiment auto-duale: elle se heurte à la
dualité entre séparation et connexité (c4 vs. c8 en 2D) et au final
des aberrations apparaissent. À la recherche d'un algorithme original
pour le calcul de l'arbre des formes, une nouvelle représentation
discrète d'images 2D est apparue. Définie sur la grille de Khalimsky
avec la topologie d'Alexandroff et s'appuyant sur l'analyse
multivoque, cette représentation a la particularité de satisfaire à de
nombreuses propriétés du continu et de s'affranchir des problèmes
topologiques classiques.
Thierry Géraud est enseignant-chercheur au Laboratoire de Recherche et
Développement de l'EPITA (LRDE), habilité à diriger les recherches.
Il est chercheur invité au laboratoire A3SI (ESIEE, LIGM,
Univ. Paris-Est Marne-la-Vallée). Il dirige le développement d'Olena,
une plateforme libre de traitement d'images. Il en utilise, conçoit
et maintient le cœur: Milena, une bibliothèque moderne, générique et
efficace, écrite en C++.
http://www.lrde.epita.fr/people/theo
Mercredi 27 mars 2013, 11-12h, Salle L-Alpha du LRDE
SMIL : Simple Morphological Image Library
- Documents
- smil.pdf
Matthieu Faessel et Michel Bilodeau, Centre de Morphologie Mathématique (Fontainebleau), Mines ParisTech
SMIL est une bibliothèque de traitement d'images 2D/3D. Elle a été
développée pour répondre à une demande de plus en plus forte (en
particulier dans le cas de projets industriels) en termes de
performances : taille d'images (2D ou 3D) et temps d'exécution.
Développée en C++ et utilisant les templates, elle peut être utilisée
avec n'importe quel type standard de données. Un effort important a
été porté sur la factorisation du code (par le biais de functors),
d'une part, pour faciliter l'intégration de nouvelles fonctions, et
d'autre part pour concentrer les parties du code permettant
l'optimisation. Ces "briques" communes optimisées utilisent le code
SIMD généré par l'auto-vectorisation de gcc et sont également
parallélisées grâce à l'utilisation d'OpenMP.
Matthieu Faessel et Michel Bilodeau sont chercheurs au Centre de
Morphologie Mathématique, Mines ParisTech. Ils travaillent dans des
domaines tels que le contrôle industriel, la vision par ordinateur,
l'étude des matériaux et le développement d'architectures logicielles
et matérielles.
http://cmm.ensmp.fr/~faessel/smil/doc/index.html, http://cmm.ensmp.fr/~faessel/
Mercredi 24 avril 2013, 11-12h, Salle L-Alpha du LRDE
Designing robust distributed systems with weakly interacting feedback structures
- Documents
- van-roy.pdf
Peter Van Roy, Université catholique de Louvain
Large distributed systems on the Internet are subject to hostile
environmental conditions such as node failures, erratic communications, and
partitioning, and global problems such as hotspots, attacks, multicast
storms, chaotic behavior, and cascading failures. How can we build these
systems to function in predictable fashion in such situations as well as
being easy to understand and maintain? In our work on building
self-managing systems in the SELFMAN project, we have discovered a useful
design pattern for building complex systems, namely as a set of Weakly
Interacting Feedback Structures (WIFS). A feedback structure consists of a
graph of interacting feedback loops that together maintain one global system
property. We give examples of biological and computing systems that use
WIFS, such as the human respiratory system and the TCP family of network
protocols. We then show the usefulness of the design pattern by applying it
to the Scalaris key/value store from SELFMAN. Scalaris is based on a
structured peer-to-peer network with extensions for data replication and
transactions. Scalaris achieves high performance: from 4000 to 14000
read-modify-write transactions per second on a cluster with 1 to 15 nodes
each containing two dual-core Intel Xeon processors at 2.66 GHz. Scalaris
is a self-managing system that consists of five WIFS, for connectivity,
routing, load balancing, replication, and transactions. We conclude by
explaining why WIFS are an important design pattern for building complex
systems and we outline how to extend the WIFS approach to allow proving
global properties of these systems.
Peter Van Roy is coauthor of the classic programming textbook "Concepts,
Techniques, and Models of Computer Programming" and professor at the
Université catholique de Louvain in Belgium. His group hosts the Mozart
Programming System (see www.mozart-oz.org), with which he explores the
relationship between programming languages and distributed programming. He
wrote the Aquarius Prolog compiler, the first to generate code competitive
in performance with C compilers. He received a M.S. and Ph.D. in Computer
Science from the University of California at Berkeley and a French
"Habilitation à Diriger des Recherches" from the Université Paris Diderot.
http://www.info.ucl.ac.be/~pvr/WIFSpaper.pdf, http://pldc.info.ucl.ac.be, http://www.mozart-oz.org, http://www.ist-selfman.org
Mercredi 22 mai 2013, 11-12h, Salle Lα du LRDE
Étendre le compilateur GCC avec MELT
- Documents
- starynkevitch.pdf
Basile Starynkevitch (CEA LIST)
Le compilateur GCC est extensible via des greffons (plugins) depuis plusieurs années. Mais c'est un logiciel libre complexe (de 10MLOC) et encore en évolution, dont on décrira grossièrement l'architecture. Écrire des greffons en C est fastidieux.
Le language d'extension MELT (domain specific language) permet d'étendre moins péniblement le compilateur GCC. Il offre une syntaxe régulière et simple, inspirée de LISP. MELT est traduit en du code C (ou C++) adapté aux internes de GCC et son implémentation (en logiciel libre) est auto-amorcée. Il offre des traits permettant des styles de programmation de haut niveau (styles fonctionnel, objet, réflexif).
On décrira un peu l'implémentation de MELT, sa syntaxe et ses traits
caractéristiques, et les exemples d'extensions.
Basile Starynkevitch est un ancien élève de l'ENS Cachan qui a soutenu sa
thèse en intelligence artificielle en 1990. Il travaille comme ingénieur
chercheur au CEA LIST dans le Laboratoire Sûreté des Logiciels (LSL), et
contribue à GCC en y développant notamment l'outil MELT. Il est un partisan
convaincu du logiciel libre.
http://gcc-melt.org/
Mercredi 29 mai 2013, 10-12h, Salle Lα du LRDE
Langages de développement et sécurité - Mind your language
- Documents
- jaeger-levillain.pdf
Eric Jaeger et Olivier Levillain, ANSSI (Agence nationale de la sécurité des
systèmes d'information)
Il existe de nombreux langages informatiques, et les débats concernant leurs
avantages et inconvénients respectifs sont nombreux, mais peu considèrent la
question du développement d'applications sécurisées, c'est-à-dire robustes
contre les actions d'agents malveillants. C'est l'optique abordée dans cette
présentation, qui rebondit sur de nombreuses illustrations dans différents
langages afin de pouvoir cerner ce que seraient les bonnes propriétés d'un
langage vis-à-vis de la sécurité, mais aussi des recommandations de codage
pertinentes ou encore des outils pertinents pour le développement et
l'évaluation d'applications de sécurité.
Eric Jaeger travaille à l'ANSSI depuis 2004. Après plusieurs années dans les laboratoires, pendant lesquelles il a notamment travaillé sur les apports et les limites des méthodes formelles pour les développements de sécurité, il est devenu chef du centre de formation à la sécurité des systèmes d'information (CFSSI). Il est à l'origine des études sur les langages commandées par l'ANSSI depuis 2008 (JavaSec sur le langage Java, et LaFoSec sur les langages fonctionnels).
Olivier Levillain travaille dans les laboratoires de l'ANSSI depuis
septembre 2007 et est aujourd'hui responsable du laboratoire sécurité des
réseaux et protocoles. Il a été l'un des promoteurs et a participé au suivi
des études JavaSec et LaFoSec entre 2008 et 2012. Il prépare également une
thèse sur la sécurité des navigateurs web, se consacrant pour l'instant
essentiellement aux protocoles SSL/TLS.
http://www.ssi.gouv.fr/fr/anssi/publications/publications-scientifiques/autres-publications/securite-et-langage-java.html, http://www.ssi.gouv.fr/fr/anssi/publications/publications-scientifiques/theses/etude-de-l-apport-des-methodes-formelles-deductives-pour-les-developpements-de.html, http://www.ssi.gouv.fr/fr/anssi/publications/publications-scientifiques/articles-de-conferences/ssl-tls-etat-des-lieux-et-recommandations.html
Mercredi 9 octobre 2013, 11h-12h, Salle Lα du LRDE
GNU epsilon, un langage de programmation extensible
- Documents
- saiu.pdf
- Keywords
- language, functional, compilation
Luca Saiu - Projet GNU, INRIA
Le réductionnisme est une technique réaliste de conception et implantation de vrais langages de programmation, et conduit à des solutions plus faciles à étendre, expérimenter et analyser. Je vais décrire la conception et l'implantation de GNU epsilon, un langage de programmation extensible, basé sur un langage-noyau minimaliste impératif du premier ordre, équipé de mécanismes d'abstraction forts et avec des possibilités de réflexion et auto-modification. Le langage peut être étendu à des niveaux très hauts: en utilisant des macros à la Lisp et des transformations de code à code réécrivant les expressions étendues en expressions-noyau, on arrive à ajouter les clôtures et les continuations de première classe au dessus du noyau.
Les programmes qui ne s'auto-modifient pas peuvent être analysés
formellement, grâce à la simplicité de la sémantique. Je vais parler
rapidement d'une analyse statique dont j'ai prouvé une propriété de
«soundness» par rapport à la sémantique dynamique. Le langage se prête à une
implantation efficace: je vais montrer un prototype de compilateur natif
particulièrement simple.
Luca Saiu, programmeur expérimenté et spécialiste de langages, a obtenu
son master à l'Université de Pise et son doctorat à l'Université Paris
13. Il a travaillé à l'INRIA sur le support multi-cœur d'OCaml. Le
langage de programmation epsilon, logiciel GNU, est son projet le plus
ambitieux. Luca Saiu est également co-auteur de Marionnet, un simulateur
de réseaux en OCaml, utilisé pour la pédagogie en France et à l'étranger.
http://www.dailymotion.com/video/k41FJWRyy1QMDm4KuIFhttp://ageinghacker.net, http://www.gnu.org/projects/epsilon
Mercredi 13 novembre 2013, 11h-12h30, Salle Lα du LRDE
Address & Thread Sanitizer dans GCC: État Actuel et Orientation Future
- Documents
- seketeli.pdf
Dodji Seketeli, Red Hat
Address & Thread sanitizer sont des outils destinés à détecter les erreurs d'accès à la mémoire ainsi que les erreurs d'accès concurrents en environnement multi-threads.
Ces outils sont constitués de deux parties logiques distinctes: une partie instrumentant le code généré de manière statique, et un environnement d'exécution.
Cet exposé présente l'implémentation de Address & Thread Sanitizer dans
GCC, les principes de fonctionnement de l'environnement d'exécution de
ces deux outils ainsi que les futures directions du projet.
Dodji Seketeli est ingénieur dans l'équipe Tools de Red Hat. Il
travaille sur la suite des compilateurs GNU, principalement sur les
compilateurs C et C++. Pendant son temps libre, lorsqu'il ne joue pas
avec son épouse et ses enfants, il maintient Nemiver, le débuggeur
graphique du projet d'environnement de bureau libre GNOME. En dehors
des logiciels libres, il s'intéresse aux arts martiaux et à l'histoire.
http://www.dailymotion.com/video/k245SpRauYYali50Ajfhttp://gcc.gnu.org, http://code.google.com/p/address-sanitizer/wiki/AddressSanitizer, http://code.google.com/p/thread-sanitizer/
Mercredi 4 décembre 2013, 11h-12h, Salle L0 du LRDE
CPC: Une implémentation efficace de la concurrence par passage de continuations
Juliusz Chroboczek, Laboratoire PPS, Université Paris-Diderot (Paris 7)
CPC est une extension concurrente du langage C. Le code CPC, en style à threads, est traduit par le compilateur CPC en un code à style à événements; ce code peut ensuite être exécuté, au choix du programmeur, par des threads natifs « lourds » ou par un ordonnanceur à événements manipulant des structures de données extrêmement légères. Cette technique d'implémentation induit un style de programmation original, où les threads sont « gratuits ». Cependant, le programmeur peut choisir d'utiliser des threads natifs « lourds » lorsque c'est nécessaire, par exemple pour exploiter le parallélisme du matériel ou utiliser des bibliothèques bloquantes.
La technique de compilation de CPC est basée sur des techniques formalisées et bien connues de la communauté de la programmation fonctionnelle, telles que la conversion en style à passage de continuations (CPS), le lambda-lifting, ou l'introduction de fonctions terminales. La correction de ces techniques a été prouvée formellement.
Dans cet exposé, je donnerai quelques exemples du style typique de
programmation en CPC tirées de Hekate, un seeder BitTorrent écrit en CPC.
Je décrirai ensuite la transformation en style à passage de continuations et
je décrirai la technique de traduction utilisée par le compilateur CPC.
Juliusz Chroboczek est Maître de Conférences à l'Université Paris-Diderot
(Paris 7). Il travaille sur les implémentations efficaces de la concurrence
ainsi que sur la problématique du routage dans les réseaux à commutation de
paquets.
http://www.pps.univ-paris-diderot.fr/~jch/software/cpc/, http://www.pps.univ-paris-diderot.fr/~jch/software/hekate/
Mercredi 11 décembre 2013, 14h-15h30, Salle L0 du LRDE
A ``Diplomatic Parallel Algorithm for the Component Trees of High Dynamic Range Images
Michael Wilkinson - Johann Bernoulli Institute, University of Groningen, The Netherlands
Component trees are essential tools in several morphological processing methods, such as attribute filtering, or visualization, or the computation of topological watersheds. Algorithms for computation of these trees fall into two main categories: (i) Flood-filling algorithms, exemplified by the algorithms of Salembier et al (1998), Hesselink (2003), and Wilkinson (2011), and (ii) Union-find methods, such as Najman and Couprie (2006), and Berger et al (2007). As images become larger, and parallel computers become commonplace, there is an increased need for concurrent algorithms to compute these trees. The first such algorithm was published by Wilkinson et al in 2008, and was based on the divide-and-conquer principle. It splits up the data spatially, computes local component trees using any arbitrary algorithm which yields a union-find type representation of each node, and glues these together hierarchically. The main drawback of this method is that it does not work well on high-dynamic-range images, because the complexity of the glueing phase scales linearly with the number of grey levels.
In the current work, carried out by Moschini, Meijster, and Wilkinson within the HyperGAMMA project, we develop a new algorithm for floating point or high-dynamic-range integer images. It works in a two-tier process, in which we first compute a pilot component tree at low dynamic range in parallel, with one grey level per processor using dynamic quantization, and Salembier's flood-filling method to build the local trees, and the previous parallellization scheme. After this, a refinement stage is performed. This refinement stage is based on the algorithm of Berger et al. As such, the new algorithm combines the two main types of algorithm in a single framework.
Timings on images of up to 3.9 GPixel indicate a speed-up of up to 22 on 64
cores. The algorithm is more than 14x faster than the fastest sequential
algorithm on the same machine. We will apply the new algorithm to
astronomical data sets, including improvements to the SExtractor tool for
object detection. The importance of the new algorithm extends beyond
computation of component trees because it allows development of a fast
alpha-tree algorithm suitable for any pixel-difference metric in case of
vector images (i.e. not just $L_\infty$-based metrics on low dynamic range
colour images).
Michael Wilkinson obtained an MSc in astronomy from the Kapteyn Laboratory,
University of Groningen in 1993, after which he worked on image analysis of
intestinal bacteria at the Department of Medical Microbiology, University of
Groningen, obtaining a PhD at the Institute of Mathematics and Computing
Science, also in Groningen, in 1995. After this he worked as a researcher at
the Johann Bernoulli Institute for Mathematics and Computer Science (JBI)
both on computer simulations and on image analysis of diatoms. He is
currently senior lecturer at the JBI, working on morphological image
analysis and especially connected morphology. Apart from publishing in
many journals and conferences, he edited the book ``Digital Image Analysis
of Microbes (John Wiley, UK, 1998) with Frits Schut, and is member of the
Steering Committee of ISMM.
http://www.cs.rug.nl/~michael/
Mercredi 5 février 2014, 11h-12h30, Salle L0 du LRDE
Programmation d'applications Web client-serveur avec Ocsigen
Vincent Balat, Université Paris Diderot et INRIA
Le Web a subi en quelques années une évolution radicale, passant d'une plateforme de données à une plateforme d'applications. Mais la plupart des outils de programmation n'ont pas été conçus pour cette nouvelle vision du Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de programmation adaptées aux besoins des sites Web modernes et des applications Web distribuées. Il permet de programmer les parties client et serveur dans le même langage, et même, comme une seule et même application. La puissance expressive du langage OCaml permet d'introduire une abstraction des technologies sous-jacentes dans le but de simplifier la programmation d'interactions Web complexes. Le système de types très avancé du langage permet d'améliorer la fiabilité des programmes et le respect des standards. Cela permet aussi de réduire beaucoup le temps de développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire un
exemple d'application simple.
Vincent Balat est maître de conférences à l'université Paris Diderot,
actuellement en délégation à l'INRIA. Il est le créateur et chef du projet
Ocsigen. Il est ancien élève de l'École Normale Supérieure de Cachan. Son
travail de recherche porte essentiellement sur l'amélioration de
l'expressivité et de la fiabilité des techniques de programmation
Web.
http://ocsigen.org
Mercredi 12 février 2014, 11h-12h30, Salle L0 du LRDE
Automates Acycliques
- Keywords
- automata
Dominique Revuz, LIGM, UMR 8046, Université Paris-Est Marne-la-Vallée
Les automates acycliques sont utilisés dans tous les logiciels de traitement de la langue naturelle essentiellement pour la représentation des lexiques, des dictionnaires et des interprétations morpho-syntaxiques des textes.
Nous présenterons des résultats sur les stratégies de construction, de
manipulation et de stockage de ces automates. En particulier un algorithme
de construction dynamique.
Docteur de l'Université Paris 7.
Directeur de l'ESIPE, école d'ingénieurs de l'université de Marne-la-Vallée.
Spécialisé en compression et représentation de données en mémoire.
http://astl.sourceforge.net/
Mardi 18 février 2014, 18h20-19h30, Amphi 4
CLAIRE : un pseudo-code élégant exécutable et compilable pour l'aide à la décision
- Documents
- caseau.pdf
- Keywords
- language
Yves Caseau, Bouygues Telecom & Académie des Technologies
CLAIRE est un langage créé il y a une vingtaine d'années pour développer, partager et enseigner des algorithmes pour la recherche opérationnelle. Notre ambition première était de créer un pseudo-code exécutable, qui permette à la fois de décrire simplement des algorithmes complexes et de les exécuter facilement, grâce à un interprète, et rapidement, grâce à un compilateur.
Après avoir brièvement rappelé l'histoire et les motivations de ce projet, la deuxième partie de l'exposé donnera des exemples de fragments de code, ainsi que quelques exemples d'applications réussies qui donnent un peu de crédit à cette ambition.
La troisième partie fera un zoom sur certaines propriétés originales de CLAIRE, qui font que ce langage de programmation conserve un certain intérêt dans le paysage de 2014. En particulier, CLAIRE permet de décrire des algorithmes d'exploration arborescents avec des mécanismes natifs de raisonnement hypothétique. Un autre intérêt de ce langage est le haut niveau de polymorphisme paramétrique, qui permet de traiter des fragments de code comme des structures de données. CLAIRE a été utilisé pour développer différents outils d'aide à la décision, de la résolution de problèmes d'optimisation combinatoire à la simulation, en particulier dans le cadre de GTES (simulation par jeux et apprentissage).
La dernière partie de cet exposé fera la liste des ressources disponibles
pour répondre à la question: pourquoi s'intéresser à un langage désuet ``20
ans après ? Le code de CLAIRE - méta-description, interprète et
plate-forme de compilation - est disponible. Une partie des fragments de
code disponibles peuvent soit servir de source d'inspiration (lorsqu'il
s'agit de fonctionnalités qui restent originales) soit de code réutilisable.
Yves Caseau est directeur général adjoint Technologie, Prospectives et Innovation à Bouygues Telecom dont il a été le DSI de 2001 à 2006. Il a commencé sa carrière dans la recherche, à Telcordia (USA) puis à la tête du e-Lab de Bouygues. Il est passé de l'intelligence artificielle à la programmation par contraintes, puis à la recherche opérationnelle pour terminer plus récemment par la simulation et la théorie des jeux.
Ancien élève de l'ENS Ulm, il est également titulaire d'un MBA du Collège
des ingénieurs, ainsi que d'un doctorat en informatique (Paris XI) et d'une
habilitation à diriger des recherches (Paris VII). Il est membre de
l'Académie des Technologies et auteur de trois livres publiés chez Dunod.
http://claire3.free.fr/, http://github.com/ycaseau/CLAIRE3.4
Mercredi 12 mars 2014, 11h-12h30, Salle L0 du LRDE
Programmation d'applications Web client-serveur avec Ocsigen
- Documents
- balat.pdf
- Keywords
- language, web, caml, functional, concurrency
Vincent Balat, Université Paris Diderot et INRIA
Le Web a subi en quelques années une évolution radicale, passant d'une plateforme de données à une plateforme d'applications. Mais la plupart des outils de programmation n'ont pas été conçus pour cette nouvelle vision du Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de programmation adaptées aux besoins des sites Web modernes et des applications Web distribuées. Il permet de programmer les parties client et serveur dans le même langage, et même, comme une seule et même application. La puissance expressive du langage OCaml permet d'introduire une abstraction des technologies sous-jacentes dans le but de simplifier la programmation d'interactions Web complexes. Le système de types très avancé du langage permet d'améliorer la fiabilité des programmes et le respect des standards. Cela permet aussi de réduire beaucoup le temps de développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire un
exemple d'application simple.
Vincent Balat est maître de conférences à l'université Paris Diderot,
actuellement en délégation à l'INRIA. Il est le créateur et chef du projet
Ocsigen. Il est ancien élève de l'École Normale Supérieure de Cachan. Son
travail de recherche porte essentiellement sur l'amélioration de
l'expressivité et de la fiabilité des techniques de programmation
Web.
Mercredi 14 mai 2014, 11h-12h30, Salle L0, LRDE
Nife : du Forth pour l'embarqué
- Keywords
- language
Patrick Foubet, gérant et directeur technique de SERIANE
Nife est un langage de programmation ``Forth-like: basé sur les principes du langage Forth, défini par Charles H. Moore dans les années 1960, il n'en reprend pas la totalité des fonctionnalités. Son ambition est d'offrir aux non-informaticiens qui ont besoin de faire des mesures, de contrôler des appareils distants, de surveiller des processus industriels, de manipuler des grandes collections de données, de faire des calculs, des filtrages, des statistiques, de pouvoir le réaliser facilement, dans un environnement Linux à faible coût.
Simple, n'importe qui peut comprendre le fonctionnement de ce langage en quelques minutes, et le maîtriser totalement en quelques heures - une semaine tout au plus. Il peut aussi être utilisé plus modestement comme une super calculatrice, pour faire ses comptes ou des calculs d'inversion de matrice. Le public concerné est donc très large.
Une extension de Nife pour les systèmes embarqués lui permet de pouvoir être
directement chargé sur de petites ou moyennes unités de calcul. Pour cela,
on lui associe un noyau ``bootable et il devient Knife : Kernelable Nife.
Dans ce cas, il devient un outil puissant pour coder dans des environnements
où la mémoire est denrée rare, et où le côté ``langage dynamique va
permettre de résoudre des problèmes là où d'autres langages vont échouer.
Patrick Foubet commence l'informatique en 1978 dans une SSII parisienne. Il y développe des applications de gestion en Cobol et en Fortran sur des main-frames IBM (DOS-VSE) et Bull (Gcos), mais aussi en assembleur sur des mini-ordinateurs Computer Automation et Data General.
En 1986 il passe au CNAM un DEA en IA. Il y enseigne ainsi qu'au CEPIA, centre de formation de l'INRIA. En 1988, il crée la société SERIANE et développe des applications industrielles : bancs de tests, acquisition de données, traitement du signal, systèmes temps-réel et embarqués. Ses clients comptent le CEA, Thomson, la RATP, Michelin, PSA, etc. C'est dans cette période qu'il crée son propre système temps-réel sous DPMI et son interface graphique SerView. En 1996, il passe au CNAM un second DEA en ``Construction de Programmes. Il apprend la Méthode B avec Jean-Raymond Abrial. Entre 2003 et 2012, il est consultant auprès du CEA/DAM dans le cadre du projet Laser MégaJoule. Dans le même temps, il enseigne dans des écoles de la région parisienne: ECE, EFREI, EPSI, ESME-Sudria, ESIGETEL, INGESUP, INSIA, ITIN, etc.
Il a libéré une partie du code qu'il a développé lors de ses travaux et
qu'il a utilisé pour écrire son langage Nife.
http://www.seriane.fr/nife/
Mercredi 11 juin 2014, 14h30-16h, Salle L0, LRDE
Méthodes rapides pour le traitement, l'analyse et la synthèse en informatique graphique
- Keywords
- image, 3d
Tamy Boubekeur, Professeur, Telecom ParisTech
L'informatique graphique 3D, qu'il s'agisse de modélisation de formes, d'analyse d'animation ou de synthèse d'images, exploite intensivement divers types de structures spatiales telles que les hiérarchies volumes englobant, les cages de déformation, les squelettes d'animation ou bien encore les structures médianes.
Dans cette présentation, je reviendrai sur quelques uns de nos travaux récents sur ce sujet. Je détaillerai notamment une nouvelle forme de représentation d'objets 3D, les Sphere-Meshes, bien adaptés à l'approximation extrême de forme et à l'auto-rigging pour la déformation interaction. Je discuterai ensuite plusieurs projets liés à l'analyse de formes, dont le système CageR pour l'ingénierie inverse de modèles issus de performance capture. J'aborderai enfin le rendu temps-réel et le calcul GPU dans le cadre l'éclairage global, qui s'appuie lui aussi sur la gestion efficace d'une structure particulière : un arbre de radiance.
À chaque étape, je donnerai des éléments sur l'implémentation pratique de
ces approches et sur les nombreux défis qu'il reste à relever.
Tamy Boubekeur est, depuis 2014, Professeur en Informatique au sein du département de Traitement du Signal et des Images de Telecom ParisTech (CNRS LTCI, Institut Mines-Telecom). Il a obtenu son doctorat à l'Université de Bordeaux, au sein de l'INRIA en 2007. De 2004 à 2007, il était chercheur invité régulier à UBC (Vancouver, Canada). En 2007, il est devenu chercheur associé à TU Berlin (Allemagne), avant de rejoindre en 2008 Telecom ParisTech en tant que Maître de Conférences, où il a créé l'équipe d'informatique graphique. Il a obtenu son Habilitation à Diriger des Recherches en 2012 à l'Université Paris XI. Il a reçu plusieurs prix scientifiques, dont le prix Gunter Enderle en 2006.
Il publie régulièrement dans les conférences internationales et journaux
majeurs de l'informatique graphique et de la vision par ordinateur.
http://www.telecom-paristech.fr/~boubek
Mercredi 19 novembre 2014, 11h30-13h, Amphi 1
Generic Tools, Specific Languages
- Documents
- voelter.pdf
Markus Voelter, independent/itemis
Generic Tools, Specific Languages is an approach for developing tools and applications in a way that supports easier and more meaningful adaptation to specific domains. To achieve this goal, GTSL generalizes programming language IDEs to domains traditionally not addressed by languages and IDEs.
At its core, GTSL represents applications as documents / programs / models
expressed with suitable languages. Application functionality is provided
through an IDE that is aware of the languages and their semantics. The IDE
provides editing support, and also directly integrates domain-specific
analyses and execution services. Applications and their languages can be
adapted to increasingly specific domains using language engineering; this
includes developing incremental extensions to existing languages or creating
additional, tightly integrated languages. Language workbenches act as the
foundation on which such applications are built.
Dr. Markus Voelter works as an independent researcher, consultant and coach
for itemis AG in Stuttgart, Germany. His focus is on software architecture,
model-driven software development and domain specific languages as well as
on product line engineering. Markus also regularly writes (articles,
patterns, books) and speaks (trainings, conferences) on those subjects.
http://www.voelter.de, http://voelter.de/books, http://mbeddr.com, mailto:voelter@acm.org
Mercredi 10 décembre 2014, 11h00-12h00, Salle L0 du LRDE
Une nouvelle approche pour la gestion de la mémoire avec CUDA
- Documents
- boissel.pdf
Raphaël Boissel, EPITA, CSI
Dans de nombreux domaines on cherche à améliorer les performances des programmes en faisant appel au « GPGPU »: un ensemble d’outils et de techniques permettant d’utiliser le GPU d’une machine afin de lui déléguer d'autres calculs que les traditionnelles routines de dessins. Cependant, écrire un programme qui exploite à la fois le GPU et le CPU n’est pas une tâche facile. Même lorsque les algorithmes se prêtent bien à la programmation GPU il arrive que le gain en performance soit décevant. L’un des principaux problèmes reste la gestion de la mémoire et surtout du transfert de données entre le GPU et le CPU. En effet l'optimisation des temps de transfert est délicate et peut nécessiter plusieurs jours d’analyse et de réécriture pour obtenir de bonnes performances.
CUDA offre de nouveaux outils pour résoudre ce problème. Des outils de profilage de code permettent de voir où se situent les problèmes de transfert. UVM (Unified Virtual Memory), le nouveau modèle de gestion de la mémoire, permet de tirer pleinement parti de CUDA bien plus facilement que par le passé.
C’est à l’utilisation de ces nouvelles techniques que nous nous intéressons
dans cette présentation.
Étudiant au LRDE dans la majeure CSI (Calcul Scientifique et Image), Raphaël
a fait son stage de fin d’étude chez NVidia, dans l’équipe CUDA driver. Il
travaillait au sein de l'équipe sur UVM sur l’implémentation de nouvelles
fonctionnalités pour ce nouveau modèle de gestion de la mémoire.
https://developer.nvidia.com/cuda-toolkit, http://docs.nvidia.com/cuda/cuda-c-programming-guide/
Mercredi 17 décembre 2014, 11h00-12h00, Salle L0 du LRDE
D’un MOOC à l'autre
- Documents
- queinnec.pdf
Christian Queinnec, UPMC, LIP6
Au printemps 2014, j'ai animé un MOOC d'initiation à l'informatique, centré
sur la programmation récursive. Bien que loin d'être massif, ce MOOC a
permis d'expérimenter ce nouveau medium ainsi que de mettre à l'épreuve une
infrastructure de correction automatisée. L'exposé portera sur ces deux
aspects et présentera également les nouveautés prévues pour la prochaine
édition de ce MOOC.
Lispeur depuis 1974, Unixien depuis 1984, HDR depuis 1988, et depuis peu
professeur émérite de l’UPMC. Surtout connu pour ses livres sur Lisp et
Scheme, il a récemment animé le MOOC « Programmation Récursive » dont il
sera question dans l’exposé.
http://lip6.fr/Christian.Queinnec/, http://programmation-recursive.net/
Mercredi 18 février 2015, 11h00-12h30, Salle L0 du LRDE
Faveod, meta-modèle au service de la qualité logicielle
- Documents
- azoury.pdf
Yann Azoury, Faveod
L’accroissement exponentiel de la complexité technique des logiciels métiers a du mal à être compensée par les progrès du génie logiciel : les coûts et les délais augmentent jusqu’à ce que l’intérêt de l’informatique soit fondamentalement remis en cause dans certains cas, arguments rationnels et légitimes à l’appui. Cette anomalie épistémologique s’explique pourtant par des erreurs technologiques récurrentes dans l’histoire, des pièges et des culs-de-sac ralentissant le progrès scientifique. Parmi ces freins : la dette technique, l’utilisation de trop de technologies, trop élitistes pour être correctement utilisées en général, et le niveau maximal de compréhension et d’analyse de chaque humain, qui est fortement variable mais toujours plafonné.
La technologie Faveod sert à éviter ces freins par la formalisation
structurée et factorisée des besoins métiers, applicatifs et techniques dans
un modèle générique et exhaustif. L’analyse continue des évolutions
collaboratives de ce modèle permet la production totalement automatisée et
instantanée de sa traduction technique : l’application cible en cohérence et
en qualité. La gestion de la complexité des facteurs influant sur la qualité
logicielle étant déléguée à la technologie, il devient possible d’augmenter
son niveau par accumulation linéaire sans dépendre des facteurs humains
limitants.
Yann Azoury, EPITA SIGL 2006, a toujours travaillé pour des éditeurs de
logiciels en France et aux Etats-Unis. En 2002, sa participation au projet
de portage d’OpenOffice pour Mac OS X pour le compte d’Apple lui permet
d'atteindre ses propres limites d’analyse et donc de comprendre la nécessité
de les dépasser par des outils. Ainsi, en 2005, il crée le projet Faveod
pour ce faire et fonde la société éponyme en 2007 pour diffuser cette
technologie.
www.faveod.com
Mercredi 11 mars 2015, 10h30-12h30, Salle L0 du LRDE
Généricité et efficacité en algèbre linéaire exacte avec les bibliothèques FFLAS-FFPACK et LinBox
- Documents
- pernet.pdf
Clément Pernet, Univ. Grenoble-Alpes, INRIA, LIP équipe AriC
Motivé par de nombreuses applications, allant de la cryptographie au calcul mathématique, le calcul formel s'est fortement développé ces dernières années tant au niveau des algorithmes que des implantations efficaces. L'efficacité des calculs repose sur celle de bibliothèques dédiées, pour certaines opérations de base, comme l'algèbre linéaire dans un corps fini ou avec des entiers multi-précision. Devant la multiplicité des domaines de calcul et des variantes algorithmiques disponibles, la conception de ces bibliothèques doit concilier une forte généricité avec l'efficacité.
Nous allons présenter comment cette problématique est abordée dans les bibliothèques d'algèbre linéaire exacte FFLAS-FFPACK (2) et LinBox (3). Après une présentation générale de ces projets, nous focaliserons la présentation sur trois aspects représentatifs:
- l'exploitation des diverses arithmétiques de base (entière, flottante, booléenne), de routines numériques optimisées et leur intégration au sein d'algorithmes génériques haut niveau ;
- l'approche boîte-noire de la bibliothèque LinBox, proposant un modèle algorithmique spécifique, particulièrement performant pour les matrices creuses ou structurées ;
- La parallélisation de code dans FFLAS-FFPACK, basée sur un langage
spécifique (DSL) permettant d'utiliser de façon interchangeable
différents langages et moteurs exécutifs, et de tirer parti du
parallélisme de tâche avec dépendance par flot de données.
Clément Pernet est maître de conférence en informatique à l'Université
Grenoble-Alpes. Sa recherche en calcul formel porte sur l'algèbre linéaire
exacte tant au niveau algorithmique que logiciel. Dans le contexte de la
fiabilité du calcul exact distribué, il aborde aussi la tolérance aux erreurs
silencieuses via les codes correcteurs d'erreurs.
(1) http://lig-membres.imag.fr/pernet, (2) http://linalg.org/projects/fflas-ffpack, (3) http://linalg.org
Multiplication matrice creuse-vecteur dense exacte et efficace.
- Documents
- boyer.pdf
Brice Boyer, UPMC CNRS INRIA, LIP6 équipe POLSYS
Tout d'abord, nous présentons un cadre générique et rapide pour les opérations SIMD (single instruction multiple data), écrit en C++ à l'intérieur de la bibliothèque d'algèbre linéaire exacte FFLAS-FFPACK (2).
Nous montrons aussi une technique de conception (modules "helper") basée sur le patron de conception Strategy, qui permet une sélection efficace d'algorithmes récursifs, des signatures de fonctions plus simples et plus uniformes. Ensuite, nous appliquons ces techniques pour accélérer la multiplication entre matrices creuses et vecteurs denses (SpMV) sur des anneaux Z/pZ, en utilisant des formats conçus pour les opérations vectorielles et en combinant diverses représentations.
Finalement, nous généralisons ces techniques aux blocs de vecteurs
(matrices denses, SpMM) et étendons nos algorithmes aux entiers de
Z. Nous appliquons aussi ces briques de base au calcul du rang de
grandes matrices creuses avec l'algorithme bloc-Wiedemann.
Brice Boyer (1) a effectué une thèse de doctorat sous la direction de
Jean-Guillaume Dumas intitulée /Multiplication matricielle efficace et
conception logicielle pour la bibliothèque de calcul exact LinBox/. Il
a ensuite effectué un post-doctorat de deux ans à la North Carolina
State University (USA) puis un autre à l'UPMC (Paris). Ses intérêts
incluent l'algèbre linéaire exacte dense et creuse, la conception et
le développement logiciels, le calcul parallèle.
(1) http://www-polsys.lip6.fr/~boyer, (2) http://linalg.org/projects/fflas-ffpack
Mercredi 13 mai 2015, 11h00-12h30, Salle L0 du LRDE
Programmation web haute performance avec C++14
- Documents
- garrigues.pdf
Matthieu Garrigues, Laboratoire d'informatique et d'ingénierie des systèmes,
ENSTA ParisTech
Le C++ est très impopulaire dans la communauté des développeurs web et ce n'est pas sans raison. Le langage n'offre aucune introspection, ce qui complique la sérialisation automatique de messages. De plus, l'injection de dépendances, un design pattern très utile dans les frameworks web issus d'autres langages, est complexe voire quasi impossible à implémenter en C++98.
Nous verrons comment l'introspection statique et l'injection de dépendance
ont été implémentés en C++14 grâce à un concept innovant: les symboles de la
bibliothèque IOD (1). Nous verrons ensuite comment Silicon (2), un jeune
framework web, tire parti de ces abstractions et aide les développeurs à
construire des APIs web aussi simplement qu'ils le feraient en Go ou
JavaScript.
Matthieu Garrigues est diplômé de la promotion CSI 2009 de l'EPITA. Depuis,
il s'intéresse au développement et l'implantation d'applications temps réel
de vision par ordinateur. Il est actuellement ingénieur de recherche et
thésard au laboratoire d'informatique et d'ingénierie des systèmes de
l'ENSTA ParisTech. Passionné par le C++ et ses nouveaux standards, il
consacre une partie de son temps libre à étudier comment le langage peut
simplifier la programmation web haute performance.
(1) https://github.com/matt-42/iod, (2) https://github.com/matt-42/silicon
Mercredi 14 octobre 2015, 11h30-12h30, Salle L0 du LRDE
Intégrales de Morton pour la Simplification Géométrique Haute Vitesse
Tamy Boubekeur, Telecom ParisTech - CNRS - University Paris-Saclay
Le traitement géométrique 3D temps-réel a progressivement atteint un niveau de performance rendant un grand nombre de primitives inspirées du traitement du signal compatible avec les applications interactives. Cela a souvent été rendu possible grâce à la co-conception des opérateurs, des structures de données et du support matériel d’exécution. Parmi les principales classes d'opérateurs géométriques, le filtrage et le sur-échantillonnage (par raffinement) ont été exprimés sous des contraintes temps-réel avec succès. Cependant, l'opérateur de sous-échantillonnage - la simplification adaptative - demeure un cas problématique pour les données non triviales.
Dans ce contexte, nous proposons un nouvel algorithme de simplification géométrique rapide basé sur un nouveau concept : les intégrales de Morton. En sommant les quadriques d'erreurs associées aux échantillons géométriques selon leur ordre de Morton, notre approche permet d'extraire de manière concurrente les nœuds correspondants à une coupe adaptative dans la hiérarchie implicite ainsi définie, et d'optimiser la position des sommets du maillage simplifié en parallèle. Cette méthode est inspirée des images intégrales et exploite les avancées récentes en construction et parcours haute performance de hiérarchies spatiales.
L'implémentation GPU de notre approche peut simplifier des maillages
composés de plusieurs millions d'éléments à un taux de rafraîchissement
interactif, tout en fournissant une géométrie simplifiée de qualité
supérieure aux méthodes uniformes et en préservant notamment les structures
géométriques saillantes. Notre algorithme est compatible avec les maillages
indexés, les soupes polygonales et les nuages de points, et peut prendre en
compte des attributs de surfaces (normal ou couleur par exemple) et des
métriques d'erreurs alternatives.
Tamy Boubekeur est Professeur en Science Informatique à Télécom ParisTech (Institut Mines-Télécom, CNRS UMR 5141, Université Paris-Saclay). Il mène ses activités de recherche dans le domaine de l’informatique graphique 3D, s'intéressant tout particulièrement à la modélisation et à la synthèse de formes, de matières et d’animation 3D numériques, mais également aux systèmes visuels interactifs à hautes performances.
De 2004 à 2007, il a été membre de l’INRIA Bordeaux (France) et chercheur
invité régulier à l’Université de Colombie Britannique à Vancouver
(Canada). Il a obtenu son Doctorat en Informatique à l’Université des
Sciences et Technologies de Bordeaux en 2007. Par la suite, il a rejoint
l’Unversité Technique de Berlin (TU Berlin) comme chercheur associé. En
2008, il a rejoint le Département de Traitement du Signal et des Images de
Télécom ParisTech comme Maître de Conférences et a créé le groupe
d’informatique graphique. Il a obtenu son Habilitation à Diriger des
Recherches (HDR) en Informatique à l’Université Paris XI en 2012 avant de
devenir Professeur à Télécom ParisTech en 2013.
http://perso.telecom-paristech.fr/~boubek/
Mercredi 27 janvier 2016, 11h-12h, Salle L0 du LRDE
Une introduction à la preuve formelle de sécurité
Pierre-Yves Strub - IMDEA Software Institute - Espagne
La cryptographie joue un rôle clé dans la sécurité des infrastructures de communication. Il est donc d'une importance capitale de construire des système cryptographiques apportant de fortes garanties de sécurité. C'est dans ce but que les constructions cryptographiques sont étudiées scrupuleusement et viennent avec une preuve de sécurité bornant la probabilité qu'un adversaire casse le crypto-système.
La majorité des preuves de sécurité sont réductionnistes: elles construisent, à partir d'un adversaire PPT (Probabilistic Polynomial-Time) violant avec une probabilité écrasante la sécurité de la construction cryptographique, un second adversaire PPT cassant une hypothèse de sécurité. Cette approche, connue sous le nom de "sécurité formelle", permet sur le principe de fournir des preuves mathématiques rigoureuses et détaillées de sécurité.
Les récentes constructions cryptographiques (et donc leur analyse de sécurité) sont de plus en plus complexes, et il n'est pas rare qu'elles incluent maintenant la preuve sécurité de l'implémentation du crypto-système, ou de sa résistance aux canaux cachés. En conséquence, les preuves de sécurité de ces algorithmes présentent un niveau de complexité tel qu'un grand nombre d'entre elles sont fausses - prouvant la sécurité d'une construction qui ne l'est pas.
Une solution prometteuse pour pallier ce problème est de développer des outils formels d'aide à la construction et vérification de crypto-systèmes. Bien que de nombreux outils existent pour la cryptographie symbolique, peu d'effort a été fait pour la cryptographie calculatoire - pourtant utilisée largement parmi les cryptographes.
Après avoir introduit le domaine de la preuve formelle et de la sécurité formelle, je présenterai EasyCrypt, un outil d'aide à la preuve des constructions cryptographiques dans le modèle calculatoire. EasyCrypt adopte une approche reposant sur la formalisation de constructions cryptographiques à partir de code concret, dans laquelle la sécurité et les hypothèses de sécurité sont modélisées à partir de programmes probabilistes et où les adversaires sont représentés par du code non spécifié. Une telle approche permet l'utilisation d'outils existants pour la vérification de programmes.
EasyCrypt est développé conjointement entre l'IMDEA Software
Institute et Inria.
Pierre-Yves Strub est chercheur au "IMDEA Software Institute", institut madrilène de recherche en informatique. En 2008, il obtient une thèse en informatique de l'École Polytechnique, puis rejoint l'équipe FORMES du laboratoire commun INRIA-Tsinghua University (Pékin, Chine). Avant d'intégrer IMDEA en 2012, il passe deux ans au laboratoire commun MSR-INRIA (Paris, France). Ses recherches portent sur les méthodes formelles, la logique en informatique, la vérification de programmes, la sécurité formelle et la formalisation des mathématiques.
Depuis qu'il a rejoint IMDEA, ses recherches portent principalement
sur la preuve formelle assistée par ordinateur en
sécurité/cryptographie. Il est l'un des principaux concepteur et
développeur d'EasyCrypt, un outil dédié à la preuve de sécurité de
constructions cryptographiques.
http://www.strub.nu, https://www.easycrypt.info/
Mercredi 17 février 2016, 11h-12h, Salle L0 du LRDE
Computing with (nearly) unlimited resources
Stephan Hadinger, Head of Solutions Architecture, AWS
Le cloud computing donne accès à des ressources de stockage et de calcul quasiment illimitées, pour un coût toujours plus bas. Devant l’explosion de la quantité des données générées et le besoin de réagir toujours plus vite, il n’a jamais été aussi facile d’accéder aux technologies de traitement massif.
Nous illustrerons de nombreux cas d’usage du cloud : Hadoop, dataware-house de plusieurs Po, traitement temps réel de millions d’événements par seconde, IOT, Machine Learning…
En particulier, l’utilisation d’algorithmes massivement parallèles
prend toute son importance et permet de tirer pleinement parti de
l’élasticité du cloud, par exemple: Monte-Carlo dans le domaine
financier, modélisation de protéines en 3D pour du screening, analyse
génomique, analyse de logs…
Stephan Hadinger a fait une longue carrière dans l'IT, spécialisé dans
les domaines Infrastructure, B2C et B2B afin de permettre aux
entreprises de tirer un maximum de bénéfices de leurs investissements
technologiques. Dans son rôle d'Architecte Solutions avec Amazon Web
Services, Stephan travaille avec des entreprises françaises de toutes
tailles pour les aider à migrer vers le Cloud et utiliser leur IT pour
mieux servir leurs clients.
https://aws.amazon.com
Mercredi 16 mars 2016, 11h-12h, Salle L0 du LRDE
Analyse hiérarchique d'images multimodales
Guillaume Tochon - Grenoble-INP & GIPSA-lab
Il y a un intérêt grandissant pour le développement d’outils de traitements adaptés aux images multimodales (plusieurs images de la même scène acquises avec différentes caractéristiques). Permettant une représentation plus complète de la scène en question, ces images multimodales ont de l'intérêt dans plusieurs domaines du traitement d'images. Les exploiter et les manipuler de manière optimale soulève cependant plusieurs questions.
Dans cet exposé, nous étendrons les représentations hiérarchiques, outil puissant pour le traitement et l’analyse d’images classiques, aux images multimodales afin de mieux exploiter l’information additionnelle apportée par la multimodalité et améliorer les techniques classiques de traitement d’images. En particulier, nous nous concentrerons principalement sur deux modalités différentes, fréquemment rencontrées dans le domaine de la télédétection:
- La modalité spectrale-spatiale, propre aux images hyperspectrales (images à très haute résolution spectrale - plusieurs centaines de canaux). Une intégration adaptée de cette information spectrale-spatiale lors de l'étape de construction de la représentation hiérarchique (en l’occurrence, un arbre de partition binaire) nous permettra par la suite, via un processus de minimisation énergétique, de proposer une carte de segmentation de l'image optimale vis-à-vis de l'opération de démélange spectral.
- La modalité sensorielle, c'est-à-dire les images acquises par des capteurs de différentes natures. Ces images "multisources", porteuses d'informations à la fois redondantes et complémentaires, sont particulièrement intéressantes pour des applications de segmentation. Nous proposerons une méthode se basant sur le très récent concept de tresses de partitions (extensions des hiérarchies de partitions classiques) afin de réaliser l'analyse hiérarchique de ces images multisources, et en obtiendrons une segmentation (là encore) via un processus de minimisation énergétique.
- Enfin, nous décrirons très brièvement une méthode d'analyse d'images
multitemporelles permettant d'effectuer du suivi d'objet, en se
basant également sur les représentations hiérarchiques des
différentes images de la séquence.
Guillaume Tochon a obtenu un diplôme d'ingénieur de Grenoble-INP
(école ENSE3) en 2012 et un doctorat de l'université de Grenoble Alpes
(rattaché au laboratoire GIPSA-lab) en 2015, tous deux en
spécialisation ``traitement du signal et des images. Il est
actuellement attaché temporaire d'enseignement et de recherche à
Grenoble-INP et conduit ses recherches au sein du département Images
et Signaux du GIPSA-lab. Ses activités de recherches se situent à
l'intersection entre la morphologie mathématique et la fusion de
données, se focalisant notamment sur l'utilisation de représentations
hiérarchiques pour l'analyse d'images multimodales, pour diverses
applications telles que la segmentation ou le démélange spectral.
Mercredi 23 mars 2016, 11h-12h, Salle L0 du LRDE
Boost.SIMD - Maximisez votre CPU directement depuis C++
Joël Falcou, Université Paris Sud, NumScale
Les extensions multimédia (SSE, AVX, NEON) sont une composante majeure des processeurs d'aujourd'hui qui restent plus que sous-utilisées. Les principales raisons de cette sous-utilisation sont la relative obscurité des jeux d'instructions, leur variété entre et même au sein des différentes familles de puces et surtout, une méconnaissance de la disponibilité des ces unités de calculs.
Boost.SIMD est une bibliothèque permettant d'exploiter ces extensions de manière efficace et expressive, facilitant l'utilisation, la diffusion et la portabilité de tels codes, ouvrant la porte à des accélérations de l'ordre de 4 à 10 sur un simple cœur.
Cet exposé présentera les fonctionnalités de Boost.SIMD, les challenges
posés par son implémentation, comment le C++ moderne répond à plusieurs de
ces problèmes et les éléments bloquants qu'il reste à résoudre.
Joël Falcou est maître de conférences en informatique au LRI, Université
Paris Sud. Ses travaux de thèse ont porté sur la programmation parallèle
pour la vision artificielle et plus particulièrement sur les applications de
la programmation générative pour la création d'outils d'aide à la
parallélisation. Il est également conseiller scientifique chez NumScale.
https://github.com/NumScale/boost.simd, https://github.com/NumScale/boost.dispatch, https://github.com/jfalcou/nt2
Mercredi 18 mai 2016, 11h-12h30, Salle L0 du LRDE
Un avant-goût de Julia
Didier Verna - EPITA/LRDE
Julia est un langage de programmation relativement jeune, développé au MIT, et vendu comme langage dynamique à haute performance pour le calcul scientifique numérique. L'un des co-auteurs du langage a une connaissance de Scheme, et Julia s'inspire en effet largement de Scheme, Common Lisp et Dylan, au point qu'il pourrait presque revendiquer un lien de parenté avec Lisp. Tout ceci est déjà suffisant pour capter notre attention, mais il y a plus: Julia semble également tirer parti de techniques modernes d'optimisation pour les langages dynamiques, en particulier grâce à son compilateur « Just-in-Time » basé sur LLVM.
Dans cette présentation, nous ferons un tour des aspects les plus
saillants du langage, avec une légère emphase sur ce qui en fait (ou
pas) un Lisp, quelques fois même (pas toujours) un meilleur Lisp que
Lisp lui-même.
Didier Verna est enseignant-chercheur au Laboratoire de Recherche et
Développement de l'EPITA. Il s'intéresse aux langages dynamiques
multi-paradigmes et en particulier aux implications de l'homoiconicité (à
tout le moins de la réflexivité) en termes de méta-programmation,
d'extensibilité et de génie logiciel en général. Didier Verna préside le
comité de pilotage du Symposium Européen sur Lisp. Il est également très
impliqué dans le logiciel libre; il fût l'un des mainteneurs d'XEmacs
pendant plus de 15 ans.
http://www.didierverna.info/, http://julialang.org
Mercredi 28 septembre 2016, 11h-12h, Salle L0 du LRDE
Transformation de la prospection commerciale grâce à la science des données
Samuel Charron
Traditionnellement, la prospection commerciale B2B se fait grâce à des listes d'entreprises classées manuellement, sur la base de données administratives renseignées à la création des entreprises. Ces listes sont donc souvent dépassées, très chères et peu qualifiées.
C-Radar, produit développé par la société Data Publica, veut transformer la prospection commerciale en enrichissant ces données administratives par des données issues du web. Ainsi, on obtient des données fraîches, plus ciblées. Et grâce aux techniques de machine learning et de clustering, on peut obtenir automatiquement des listes d'entreprises pertinentes à faible coût.
Lors de cette présentation, nous aborderons les différentes techniques
de science des données mises en œuvre dans ce produit, en relation
avec les fonctionnalités du produit.
Diplomé CSI 2008, Samuel Charron a travaillé chez différents éditeurs
logiciels, toujours autour du thème de l'exploitation et de la
valorisation des données issues du web.
http://samuelcharron.fr
Mercredi 23 novembre 2016, 11h-12h, Salle L0 du LRDE
Analyse du mouvement avec applications bio-médicales
Elodie Puybareau, LIGM
L’analyse du mouvement, ou l’analyse d’une séquence d’images, est l’extension naturelle de l’analyse d’images à l’analyse de séries temporelles d’images. De nombreuses méthodes d’analyse de mouvement ont été développées dans le contexe de vision par ordinateur, comprenant le suivi de caractéristiques, le flot optique, l’analyse de points-clefs, le recalage d’image, etc.
Dans cet exposé, nous présenterons les outils que nous avons
développés pour l'analyse de mouvement adaptés à l’analyse de séquences
biomédicales, et en particulier pour les cellules ciliées. Ces cellules,
couvertes de cils qui battent, sont présentes chez l’homme dans les zones
nécessitant des mouvements de fluide. Dans les poumons et les voies
respiratoires supérieures par exemple, les cils sont responsables de l’épuration
muco-ciliaire, qui permet d’évacuer des poumons la poussière et autres
impuretés inhalées. Les altérations de l’épuration muco-ciliaire peuvent
être liées à des maladies génétiques ou acquises. Ces maladies, touchant les cils,
sont potentiellement handicapantes. Elles peuvent cependant être
caractérisées par l’analyse du mouvement des cils sous un microscope, avec
une résolution temporelle importante. Nous avons développé plusieurs outils
et techniques pour réaliser ces analyses de manière automatique et avec
une haute précision.
Elodie Puybareau est en thèse d'Imagerie Bio-Médicale depuis le 1er
décembre 2013 au LIGM. Ses travaux portent surtout sur l’analyse du
mouvement à partir de vidéos, afin d'en extraire divers paramètres qui
s'appliquent à des sujets bio-médicaux.
http://ciliola.fr
Mercredi 7 décembre 2016, 11h-12h, Salle L0 du LRDE
Des données spatio-temporelles aux dynamiques urbaines
Julien Perret, équipe COGIT, LaSTIG, IGN
La ville est un système complexe façonné par des dynamiques opérant à des échelles différentes. En tant que chercheur en sciences de l'information géographique travaillant dans l'interdisciplinarité, je travaille en collaboration avec des spécialistes du transport, des géographes, des urbanistes, des historiens, des démographes, et des physiciens, afin de proposer de meilleurs outils, modèles et données pour l'étude multi-échelle des dynamiques urbaines.
Je présente mes contributions dans un ordre correspondant à l'échelle spatiale, de la plus large à la plus fine : la très grande échelle pour les questions liées à la mobilité, la grande échelle pour celles liées à l'urbanisme et la petite échelle pour les questions liées à l'évolution du territoire sur le long terme.
Pour chaque partie, je vais m'attacher à proposer un cheminement commun :
tout d'abord la question des sources d'information, des connaissances
manipulées, leur représentation, leur stockage ; ensuite, la question de
l'analyse de ces données, de leur enrichissement, de leur croisement ;
enfin, l'interaction avec ces données, leur visualisation, leur
interprétation, leur validation, leur correction par des utilisateurs.
Julien Perret (Dr. Université de Rennes 1 2006) est chercheur en
Informatique et en Sciences de l'Information Géographique au sein de
l'équipe de Cartographie et Géomatique (COGIT) du Laboratoire des Sciences
et Technologies de l'Information Géographique (LaSTIG) de l'Institut National
de l'Information Géographique et Forestière (IGN). Ses sujets de recherche
portent principalement sur les données spatio-temporelles et en particulier
les données géo-historiques, l'appariement de données géographiques et
géo-historiques, la simulation urbaine 2D et 3D, la modélisation des
systèmes complexe et l'optimisation stochastique. Il contribue à la mise en
place de nouveaux standards pour la recherche reproductible par la
diffusion des travaux de recherche sous la forme de données libres et de
logiciels libres.
http://recherche.ign.fr/labos/cogit/cv.php?prenom=Julien&nom=Perret, https://geohistoricaldata.org
Mercredi 18 janvier 2017, 11h-12h, Salle L0 du LRDE
Analyse topologique de données pour la visualisation scientifique: où en est-on et où va-t-on?
Julien Tierny - CNRS - LIP6 - UPMC
La visualisation scientifique est un domaine qui vise à aider les utilisateurs à (i) représenter, (ii) explorer et (iii) analyser des données géométriques acquises ou simulées, à des fins d'interprétation, de validation ou de communication. Parmi les techniques existantes, les algorithmes inspirés par la théorie de Morse ont démontré leur utilité dans ce contexte pour l'extraction efficace et robuste de structures d'intérêts, et ce, à plusieurs échelles d'importance.
Dans cette présentation, je donnerai un bref tutoriel sur l'analyse
topologique de champs scalaires, en introduisant quelques concepts clés comme
celui de graphe de Reeb, de complexe de Morse-Smale ou de diagramme de
persistance. Par ailleurs, j'illustrerai ces notions par des cas
d'applications concrets en astrophysique, chimie moléculaire ou
encore en combustion.
Ensuite, je discuterai certaines problématiques pratiques ayant récemment
émergé avec le développement des ressources de calcul haute-performance. Ces
problématiques induisent non seulement des jeux de données d'une taille
inédite, mais également des types nouveaux de données, comme les champs
scalaires multivariés ou incertains. Ces difficultés ne sont pas uniquement
intéressantes pour la communauté de recherche à cause de leur forte importance
pratique, mais aussi parce qu'elles nécessitent un redémarrage complet de
l'effort de recherche entrepris dans ce domaine ces vingt dernières années. En
particulier, je présenterai de nouvelles directions de recherche, étayées par
des résultats préliminaires récents concernant l'analyse topologique dans un
contexte de calcul haute-performance, ainsi que l'analyse topologique de
champs scalaires incertains ou bivariés.
Julien Tierny a obtenu un Doctorat en informatique de l'Université Lille 1 en 2008,
et l'Habilitation à Diriger des Recherches de l'Université Pierre-et-Marie-Curie en 2016.
Depuis septembre 2014, il est chercheur permanent au CNRS, affilié avec le laboratoire LIP6
(UPMC), après avoir été chercheur à Télécom ParisTech entre 2010 et 2014.
Avant cela, lauréat d'une bourse Fulbright, il a été chercheur associé en
post-doctorat au Scientific Computing and Imaging Institute de l'Université d'Utah.
Ses intérêts de recherche comprennent l'analyse topologique et géométrique de données
pour la visualisation scientifique. Il a reçu en 2016 la "Mention Honorable" du concours
IEEE Scientific Visualization Contest ainsi que le prix du meilleur article
de la conférence IEEE VIS.
http://lip6.fr/Julien.Tierny
Mercredi 8 février 2017, 13h30-15h00, Salle L0 du LRDE
Vcsn : une visite guidée
Akim Demaille, LRDE
Vcsn est une plateforme consacrée aux automates et aux expressions rationnelles. Parce qu'elle traite une large variété de natures d'automates, elle place en son coeur le concept de "contexte", qui type les automates, les expressions rationnelles, etc. La plateforme repose sur une bibliothèque C++14 "templatée" par des contextes, au dessus de laquelle la couche "dyn" qui, grâce à de l'effacement de type et de la compilation à la volée, offre à l'utilisateur le confort d'une bibliothèque traditionnelle avec la généricité et les performances d'une bibliothèque templatée. Ces bibliothèques sont ensuite exposées au travers d'outils en ligne de commande, mais aussi Python et surtout IPython, qui permettent une exploration interactive simple d'algorithmes. La bibliothèque Vcsn repose sur un ensemble d'objets - automates, étiquettes, poids, polynômes, expressions rationnelles et développements rationnels - sur lesquels sont fournis plus de trois cents algorithmes. Dans certains cas, Vcsn offre des fonctionalités inégalées, et certains de ces algorithmes ont des performances supérieures à celles des projets comparables.
Nous ferons une présentation de l'architecture générale de Vcsn, sous
la forme d'une démonstration guidée par les questions, ainsi qu'un
exposé des objectifs de Vcsn 3.0.
Akim Demaille est enseignant-chercheur à l'EPITA depuis pratiquement la
création du LRDE. Il y a enseigné la logique, la théorie des
langages, la construction des compilateurs, la modélisation
orientée-objet et la programmation en C++. Depuis 2013, il investit
son temps de recherche dans la plateforme Vcsn. Il a également
contribué à divers logiciels libres, tels GNU Autoconf, GNU Automake,
GNU Bison et même GNU a2ps, à un temps où ASCII et PostScript
n'étaient pas l'un et l'autre obsolètes.
http://vcsn.lrde.epita.fr
Un outil en ligne de manipulation d'automates et de semi-groupes
Charles Paperman, Université Paris Diderot
Je présenterai un outil en ligne dont l'objectif est de manipuler et
tester des propriétés algébriques pour des automates. Une courte
présentation de la théorie algébrique des automates sera donnée à la
volée. Les seuls concepts nécessaires à la compréhension de l'exposé
sont les expressions régulières, ainsi que la minimisation et la
déterminisation d'automates finis.
Charles Paperman a fini son doctorat en 2013 sous la direction de
Jean-Éric Pin et Olivier Carton, au LIAFA, et travaille désormais au
laboratoire de Logique Mathématique de l'Université Paris Diderot avec Arnaud Durand.
Ses sujets d'étude s'articulent autour de la logique, la théorie des
automates, et la complexité des circuits, avec une approche
algébrique.
paperman.cadilhac.name/pairs
Mercredi 22 février 2017, 11h-12h, Salle L0 du LRDE
Extraction de biomarqueurs des troubles autistiques à partir de l'activité cérébrale (IRMf) par apprentissage de dictionnaire parcimonieux.
Alexandre Abraham, INRIA
L'Imagerie par Résonance Magnétique fonctionnelle (IRMf) est une source
prometteuse de biomarqueurs permettant le diagnostic de troubles
neuropsychiatriques sur des sujets non coopératifs.
L'IRMf s'étudie en établissant un atlas de régions cérébrales représentatif
de l'organisation fonctionnelle, puis en étudiant la corrélation entre leurs
signaux.
Pour les extraire, nous proposons une approche d'apprentissage de
dictionnaire multi-sujets intégrant une pénalité imposant compacité spatiale et
parcimonie.
Nous sélectionnons les unités de base des réseaux fonctionnels
extraits à l'aide de techniques de segmentation inspirées du domaine de la
vision. Nous montons à l'échelle sur de gros jeux de données en utilisant
une stratégie d'optimisation stochastique.
A défaut de vérité terrain, nous proposons d'évaluer les modèles générés
à l'aide de métriques de stabilité et de fidélité.
Nous intégrons ensuite notre méthode de définition de régions dans un
pipeline entièrement automatisé, afin de réaliser une tâche de diagnostic des troubles
autistiques à travers différents sites d'acquisition et sur des
sous-ensembles d'homogénéité variable. Nous montrons que nos modèles ont une meilleure
performance, à la fois relativement aux métriques d'évaluation mais également sur nos
résultats expérimentaux.
Enfin, par une analyse post-hoc des résultats, nous montrons que la
définition de région est l'étape la plus importante du pipeline et que l'approche que
nous proposons obtient les meilleurs résultats. Nous fournissons également
des recommandations sur les méthodes les plus performantes pour les autres
étapes du pipeline.
Alexandre Abraham est un ancien de la promo CSI 2009. Il a notamment
travaillé sur le watershed topologique et les espaces couleur pour le projet Olena. Après
l'EPITA, il a suivi un master IAD à l'UPMC et a réalisé sa thèse à l'INRIA sur la
segmentation de signaux fonctionnels cérébraux au repos sur de grandes cohortes à des fins de
diagnostic. Il travaille aujourd'hui dans l'équipe de recommandation de produits chez
Criteo.
http://nilearn.github.io/, http://www.twinee.fr
Mercredi 8 mars 2017, 11h-12h, Salle L0 du LRDE
Calcul parallèle pour problèmes inverses
Nicolas Gac, Université Paris Sud, L2S (Centrale Supélec, CNRS)
Les algorithmes itératifs utilisés lors de la résolution de problèmes inverses portant sur des gros volumes de données requièrent
une accélération significative pour être utilisés en pratique. Sur des exemples d'applications en tomographie X et
en déconvolution de signaux 1D (enregistrement sur plusieurs années de données spectrales de Mars) ou 2D (flux vidéo d'une webcam),
nous présenterons notre recherche de solutions permettant la parallélisation des calculs la plus efficace possible
sur les processeurs de type "many cores" que sont les GPUs. Nous exposerons ainsi la triple adéquation entre
l'architecture des processeurs GPUs (CUDA de Nvidia), la (re)formulation des algorithmes et la (re)structuration
des données que nous avons mises en oeuvre sur différents types d'opérateurs utilisés dans les algorithmes
itératifs (projecteur, rétroprojecteur, convolution nD). Par ailleurs, nous montrerons l'attention particulière
qui doit être apportée au goulot d'étranglement lié au temps de transfert entre le PC et les cartes GPUs.
Enfin, nous présenterons le découpage des données que nous avons effectué afin de bénéficier pleinement
d'un serveur multi-GPUs et apporterons quelques éléments de réponse sur l'utilisation des GPUs couplés à Matlab
et des bibliothèques déjà existantes (CUBLAS, NVPP...).
Nicolas Gac est maître de conférences à l'université Paris Sud. Après avoir effectué sa thèse au Gipsa-lab, à Grenoble, en adéquation
algorithme architecture pour la reconstruction tomographique, il poursuit ses travaux de recherche au laboratoire des Signaux et
Systèmes (L2S) sur le calcul parallèle pour les problèmes inverses sur serveurs de calculs multi-GPUs ou FPGA. Les domaines
applicatifs de ses travaux sont la reconstruction tomographique, la reconnaissance radar, la localisation de sources acoustiques
et le traitement de données spectrales de Mars.
http://webpages.lss.supelec.fr/perso/nicolas.gac/francais/index.html
Mercredi 3 mai 2017, 11h-12h, Amphi 3 de l'EPITA
Apprentissage par Imitation Auto-Supervisée
Pierre Sermanet, Google Brain
Nous proposons une approche auto-supervisée pour l’apprentissage de
représentations à partir de vidéos non supervisées, enregistrées à de
multiples points de vue. Cette approche est particulièrement pertinente en
robotique pour l’apprentissage par l’imitation, qui nécessite une
compréhension invariante par rapport au point de vue des relations
entre les humains et leur environnement (telles que les interactions
entre objets, les attributs et les poses corporelles). Nous entraînons
nos représentations à l’aide d’une stratégie de type triplet loss,
où les multiples points de vue simultanés de la même observation
sont attirés dans l’espace d’intégration, tout en étant repoussés
des voisins temporels qui sont souvent visuellement similaires mais
fonctionnellement différents. Ce signal encourage notre modèle à
découvrir des attributs invariants vis-à-vis du point de vue, mais
qui varient dans le temps, tout en ignorant les potentielles nuisances
telles que les occlusions, le flou de mouvement, l’éclairage et
l’arrière-plan. Nos expériences démontrent qu’une telle représentation
acquiert même un certain degré d’invariance vis-à-vis de l’instance
d’objet. Nous montrons que notre modèle peut correctement identifier
les étapes correspondantes dans les interactions complexes d’objets,
à travers différentes vidéos avec différentes instances. Nous montrons
également les premiers résultats, à notre connaissance, d’apprentissage
intégralement auto-supervisé pour l’imitation de mouvements humains
par un robot réel.
Pierre Sermanet est issu de la promo EPITA 2005 (spécialisation GISTR). En
2004 il participe avec Evolutek à la compétition robotique Eurobot
<http://cs.nyu.edu/~sermanet/eurobot.html>. Après son stage de fin d’étude
chez Siemens Research à Princeton, il travaille avec Yann LeCun en tant
qu’ingénieur de recherche pendant 3 ans sur le thème du deep learning pour
le projet de robotique mobile LAGR <http://cs.nyu.edu/~sermanet/lagr.html>.
Il effectue ensuite son doctorat en deep learning avec Yann LeCun à l'Université
de New York jusqu’en 2013, puis il rejoint ensuite Google Brain en tant que
chercheur en deep learning appliqué à la vision et à la robotique.
https://sermanet.github.io/tcn/
Mercredi 14 juin 2017, 11h-12h, Salle L0 du LRDE
MAQAO: une suite d'outils pour l'analyse et l’optimisation des performances
Andrés S. Charif Rubial (ESN PeXL et Li-PARAD - Université de Versailles)
MAQAO (Modular Assembly Quality Analyzer and Optimizer) est une suite d'outils d'analyse et d'optimisation des performances
à destination d'applications binaires. Le but principal de MAQAO est d'analyser des codes binaires puis de proposer aux
développeurs d'applications des rapports synthétiques les aidant à comprendre et optimiser les performances de leur application.
MAQAO combine des analyses statiques (évaluation de la qualité du code) et dynamiques (profiling) basées sur la capacité
à reconstruire des structures aussi bien bas niveau (basic blocks, instructions, etc.) que haut niveau (fonctions et boucles).
Un autre aspect important de MAQAO est son extensibilité. En effet les utilisateurs peuvent écrire leur propre plugin
grâce à un langage de script simple intégré (Lua).
Le Dr. Andres S. CHARIF RUBIAL dirige aujourd'hui une ESN dont les principales activités sont le HPC, l’ingénierie système,
réseau et sécurité. En parallèle il est chercheur hébergé au Laboratoire Li-PARAD de l'Université de Versailles.
Il a dirigé pendant 4 ans l'équipe de recherche et développement "évaluation des performance" du laboratoire
Exascale Computing Research Laboratory (situé sur le campus Teratec). Il a principalement supervisé et travaillé au développement
de la suite d'outils MAQAO afin de mieux comprendre les problèmes de performance des applications HPC mono et multi-noeuds.
Ses travaux de thèse achevés en 2012 portaient d'ailleurs déjà sur cette thématique, en particulier sur le profilage d'applications
et les problématiques de caractérisation des performances mémoire sur des systèmes à mémoire partagée.
www.maqao.org, www.pexl.eu
Mercredi 27 septembre 2017, 11h-12h, Salle L0 du LRDE
Frama-C, une plateforme collaborative et extensible pour l'analyse de code C
Julien Signoles, CEA LIST, Laboratoire de Sûreté des Logiciels (LSL)
Frama-C est une plateforme d'analyse de code C visant à vérifier des programmes C de taille industrielle. Elle fournit à ses utilisateurs une collection de greffons effectuant notamment des analyses statiques par interprétation abstraite et des méthodes déductives ou encore permettant des vérifications à l'exécution. La plateforme permet également de faire coopérer les analyses grâce au partage d'un noyau et d'un langage de spécification communs.
Cet exposé présente une vue générale de la plateforme, de ses principaux
analyseurs et de quelques applications industrielles. Il se concentre sur le
langage de spécification ACSL et sur différentes façons de vérifier des
spécifications ACSL avec des analyses statiques ou dynamiques.
Julien Signoles a obtenu un doctorat en informatique de l'Université
Paris 11 en 2006. Il devint ensuite ingénieur-chercheur au CEA LIST
en 2007. Au sein du Laboratoire de Sûreté des Logiciels (LSL), il est l'un des
développeurs principaux de Frama-C. Ses recherches se concentrent aujourd'hui
sur la vérification à l'exécution (runtime verification) et ses différentes
applications pour améliorer la sûreté et la sécurité des logiciels critiques.
orateur : http://julien.signoles.free.fr, projet : http://frama-c.com
Mercredi 8 novembre 2017, 10h-12h, Amphi 4 de l'EPITA
Lire les lignes du cerveau humain
Jean-François Mangin, NeuroSpin, CEA, Paris-Saclay
La lecture des lignes de la main est une activité ancestrale sans
fondement scientifique, même si certains motifs sont associés à des
malformations congénitales comme la trisomie 21. Cette conférence
décrira l’émergence d’une véritable science de la lecture des « lignes
du cerveau humain », qu’il s’agisse des plissements de son cortex ou
de la trajectoire des faisceaux de fibres qui constituent son câblage
à longue distance. Des formes inhabituelles de ces plissements ou de
ces faisceaux sont parfois la trace d’anomalies développementales
susceptibles d’augmenter le risque de développer certaines
pathologies.
Jean-François Mangin est directeur de recherche au CEA. Il y dirige un
groupe de recherche algorithmique en neuro-imagerie au sein du centre
Neurospin, la plateforme IRM en champs intenses du CEA. Il est aussi
directeur du CATI, la plateforme française créée par le plan Alzheimer
pour prendre en charge les grandes études de neuroimagerie
multicentriques. Il est enfin codirecteur du sous-projet «Human
Strategic Data» du Human Brain Project, le plus vaste projet de
recherche de la commission européenne. Il est ingénieur de l’Ecole
Centrale Paris et Docteur de Télécom ParisTech. Son programme de
recherche vise au développement d’outils de vision par ordinateur
dédiés à l’interprétation des images cérébrales. Son équipe
s’intéresse en particulier aux anomalies des plissements ou de la
connectivité du cortex associées aux pathologies. Elle distribue les
outils logiciels issus de cette recherche à la communauté.
www.cati-neuroimaging.com, www.humanbrainproject.eu, www.brainvisa.info
Apprentissage automatique en neuroimagerie: application aux maladies cérébrales
Edouard Duchesnay, NeuroSpin, CEA, Paris-Saclay
L'apprentissage automatique, ou "pattern recognition" multivarié, peut
identifier des motifs complexes, associés à une variable d'intérêt, et
ce, dans des données de grandes dimensions. Une fois l'apprentissage
effectué par l'algorithme, il est appliqué à un nouvel individu afin
de prédire l'évolution future de ce dernier. L'imagerie par résonance
magnétique (IRM) fournit une approche efficace et non invasive pour
étudier les changements structurels et fonctionnels du cerveau,
associés aux conditions cliniques des patients. En combinant
apprentissage automatique et imagerie cérébrale, il est possible de
considérer l'émergence d'une médecine personnalisée, où les
algorithmes ont appris du passé à prédire la réponse probable et
future d'un patient donné à un traitement spécifique. Ces nouvelles
informations guideront le clinicien dans ses choix thérapeutiques.
Nous présenterons la complexité des données IRM manipulées, les
algorithmes d'apprentissage et leurs applications aux maladies
cérébrales.
Edouard Duchesnay a obtenu un diplôme d'ingénieur en génie logiciel de
l'EPITA en 1997 (spécialisation SCIA), puis un master et un doctorat
en traitement du signal et des images de l'Université de Rennes 1,
respectivement en 1998 et 2001. Depuis 2008, il est chargé de
recherche chez Neurospin, le centre de neuroimagerie par IRM du
CEA. Il développe des algorithmes d'apprentissage automatique
fournissant des outils de diagnostic et pronostic ou des méthodes de
découverte de biomarqueurs pour les maladies du cerveau. E. Duchesnay
est un contributeur majeur de la bibliothèque d'apprentissage
automatique ParsimonY de Python, dédiée aux données structurées de
grandes dimensions, telles que l'imagerie cérébrale ou les données
génétiques. Il a également contribué à la bibliothèque d'apprentissage
automatique scikit-learn de Python.
Home page: https://duchesnay.github.io/, ParsimonY library https://github.com/neurospin/pylearn-parsimony, Scikit-learn library http://scikit-learn.org
Mercredi 29 novembre 2017, 10h-11h, Amphi 4 de l'EPITA
Industrial Formal Verification – Cadence’s JasperGold Formal Verification Platform
Barbara Jobstmann, Cadence Design Systems
Formal verification (aka Symbolic Model Checking) is becoming a
mainstream technology in system on a chip (SoC)/intellectual property
design and verification methodologies. In the past, the usage of
formal verification was limited to a small range of applications; it
was mainly used to verify complex protocols or intrinsic logic
functionality by formal verification experts. In recent years, we saw
a rapid adoption of formal verification technology and many new
application areas, such as checking of configuration and status
register accesses, SoC connectivity verification, low power design
verification, security applications, and many more. In this talk, we
give an overview of the JasperGold Formal Verification Platform. The
platform provides a wide range of formal apps, which ease adoption of
formal verification by offering property generation and other targeted
capabilities for specific design and verification tasks. In addition,
JasperGold offers a unique interactive debug environment (called
Visualize) that allows the user to easily analyze the verification
results. We present JasperGold from a user’s point of view, showcase
selected apps, and discuss features that were essential for their wide
adoption.
Barbara Jobstmann is a field application engineer for Cadence Design
Systems and a lecturer at the École Polytechnique Fédérale de Lausanne
(EPFL). She joined Cadence in 2014 through the acquisition of Jasper
Design Automation, where she worked since 2012 as an application
engineer. In the past, she was also a CNRS researcher (chargé de
recherche) in Verimag, an academic research laboratory belonging to
the CNRS and the Communauté Université Grenoble Alpes in France. Her
research focused on constructing correct and reliable computer systems
using formal verification and synthesis techniques. She received a
Ph.D. degree in Computer Science from the University of Technology in
Graz, Austria in 2007.
Mercredi 13 décembre 2017, 11h-12h, Amphi 4 de l'EPITA
Vers l'apprentissage d'un sens commun visuel
Camille Couprie, Facebook AI research
Les réseaux de neurones convolutifs connaissent depuis quelques années un franc succès dans de nombreuses applications de reconnaissance visuelle. Nous reviendrons sur les premiers travaux en la matière en segmentation sémantique (étiquetage de chaque pixel des images par une catégorie sémantique). Nous explorerons ensuite une piste d'amélioration visant à réduire la quantité de données labelisées utilisée, à base d'entraînement de réseaux adversaires.
Dans un second temps, nous nous intéresserons au problème de la
prédiction d'images suivantes dans les vidéos: s'il nous parait
simple d'anticiper ce qu'il va se passer dans un futur très proche,
c'est un problème difficile à modéliser mathématiquement étant données
les multiples sources d'incertitude. Nous présenterons nos travaux de
prédiction dans le domaine des images naturelles, puis dans l'espace
plus haut niveau des segmentations sémantiques, nous permettant de
prédire plus loin dans le futur.
Camille Couprie est chercheuse à Facebook Artificial Intelligence
Research. Elle a obtenu son doctorat en informatique de l'Université
Paris Est en 2011, sous la direction de Hugues Talbot, Laurent Najman
et Leo Grady, avec une recherche spécialisée dans la formulation et
l'optimisation de problèmes de vision par ordinateur dans les graphes.
En 2012, elle a travaillé comme postdoc a l'institut Courant de New
York University avec Yann LeCun. Après un poste IFP new energies,
organisme de recherche français actif dans les domaines de l'énergie,
des transports et de l'environnement, elle a rejoint Facebook en 2015.
https://perso.esiee.fr/~coupriec/, http://cs.nyu.edu/~mathieu/iclr2016.html, http://thoth.inrialpes.fr/people/pluc/iccv2017
Mercredi 30 mai 2018, 11h-12h, Amphi IP11
Partial but Precise Loop Summarization and Its Applications
Jan Strejcek, Masaryk University
We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on program variables. For a program variable, the algorithm produces an expression representing the variable value after the number of cycle iterations specified by parameters of the expression. The algorithm is partial in the sense that it can fail to find such an expression for some program variables (for example, it fails in cases where the variable value depends on the order of paths in the cycle taken during iterations).
We present two applications of this loop summarization procedure. The
first is the construction of a nontrivial necessary condition on program
input to reach a given program location. The second application is a
loop bound detection algorithm, which produces tighter loop bounds than
other approaches.
Jan Strejcek is an associate professor at the Faculty of Informatics
of Masaryk University located in Brno, Czech Republic. He received his
PhD in Computer Science (2005) and Master degrees in Mathematics
(2000) and Computer Science (2001) from the same university. His
current research focuses on automata over infinite words, automatic
program analysis, and SMT-solving of quantified bitvector formulae.
https://www.fi.muni.cz/~xstrejc/
Mercredi 13 juin 2018, 11h-12h, Amphi 401
Hierarchical image representations: construction, evaluation and examples of use for image analysis
Camille Kurtz (LIPADE, Université Paris Descartes)
Hierarchical image representations have become increasingly popular in
image processing and computer vision over the past decades. Indeed,
they allow a modeling of image contents at different (and
complementary) levels of scales, resolutions and semantics. Methods
based on such image representations have been able to tackle various
complex challenges such as multi-scale image segmentation, image
filtering, object detection, recognition, and more recently image
characterization and understanding. In this talk, we will focus on the
binary partition tree (BPT), which is a well-known hierarchical
data-structure, frequently involved in the design of image
segmentation strategies. In a first part, we will focus on the
construction of such trees by providing a generalization of the BPT
construction framework to allow one to embed multiple features, which
enables handling many metrics and/or many images. In a second part,
we will discuss how it may be possible to evaluate the quality of such
a structure and its ability to reconstruct regions of the image
corresponding to segments of reference given by a user. Finally, we
will see some examples of image analysis and recognition processes
involving these hierarchical structures. The main thematic application
is remote sensing and satellite image analysis.
Camille Kurtz obtained the MSc and PhD from Université de Strasbourg,
France, in 2009 and 2012. He was a post-doctoral fellow at Stanford
University, CA, USA, between 2012 and 2013. He is now an Associate
Professor at Université Paris Descartes, France. His scientific
interests include image analysis, data mining, medical imaging and
remote sensing.
www.math-info.univ-paris5.fr/~ckurtz/
Mercredi 4 juillet 2018, 11h-12h, Amphi IP11
Y a-t-il une théorie de la détection des anomalies dans les images digitales?
Jean-Michel Morel (École Normale Supérieure Paris-Saclay)
Dans ce travail en collaboration avec Axel Davy, Mauricio Delbracio et
Thibaud Ehret, je passerai en revue les classes d'algorithmes dont le
but est de détecter des anomalies dans les images digitales. Ces
détecteurs répondent au difficile problème de trouver automatiquement
des exceptions dans des images de fond, qui peuvent être aussi
diverses qu'un tissu ou une mammographie. Des méthodes de détection
ont été proposées par milliers car chaque problème nécessite un modèle
de fond différent. En analysant les approches existantes, nous
montrerons que le problème peut être réduit à la détection d'anomalies
dans les images résiduelles (extraites de l'image cible) dans
lesquelles prédominent le bruit et les anomalies. Ainsi, le problème
général et impossible de la modélisation d'un fond arbitraire est
remplacé par celui de modèliser un bruit. Or un modèle de bruit permet
le calcul de seuils de détection rigoureux. L'approche au problème
peut donc être non supervisée et fonctionner sur des images
arbitraires. Nous illustrerons l'usage de la théorie de détection dite
a contrario, qui évite la sur-détection en fixant des seuils de
détection prenant en compte la multiplicité des tests.
Mathématicien de formation, docteur de l'Université Pierre et Marie
Curie, Assistant à Marseille-Luminy, maître de conférences et
professeur à l'Université Paris-Dauphine puis à l'ENS Cachan, JMM a
fait ses premiers travaux sur les équations aux dérivées partielles
non-linéaires et les méthodes variationnelles. Il s'est ensuite
consacré au développement d'outils mathématiques pour le traitement et
l'analyse d'images et la modélisation de la perception visuelle.
https://sites.google.com/site/jeanmichelmorelcmlaenscachan/
Vendredi 14 décembre 2018, 11h-12h, Amphi IP12A
Toward myocardium perfusion from X-ray CT
Clara Jaquet (ESIEE Marne-la-Vallée)
Recent advances in medical image computing have resulted in automated systems that closely assist physicians in patient
therapy. Computational and personalized patient models benefit diagnosis, prognosis and treatment planning, with a
decreased risk for the patient, as well as potentially lower cost. HeartFlow Inc. is a successful example of a company
providing such a service in the cardiovascular context. Based on patient-specific vascular model extracted from X-ray CT
images, they identify functionally significant disease in large coronary arteries. Their combined anatomical and
functional analysis is nonetheless limited by the image resolution. At the downstream scale, a functional exam called
Myocardium Perfusion Imaging (MPI) highlights myocardium regions with blood flow deficit. However, MPI does not
functionally relate perfusion to the upstream coronary disease. The goal of our project is to build the functional
bridge between coronary and myocardium. To this aim we propose an anatomical and functional extrapolation. We produce an
innovative vascular network generation method extending the coronary model down to the microvasculature. In the
resulting vascular model, we compute a functional analysis pipeline to simulate flow from large coronaries to the
myocardium, and to enable comparison with MPI ground-truth data.
After completing a technological university degree in biology at Creteil, Clara Jaquet obtained the diploma of
biomedical engineer from ISBS (Bio-Sciences Institute) in 2015. She worked for one year at HeartFlow Inc, California,
before starting a PhD at ESIEE, Université Paris-Est, within the LIGM laboratory, on a research project jointly with the
same company.
Mercredi 6 mars 2019, 11h - 12h, Amphi 4
Restauration de la vision grâce aux implants rétiniens
Vincent Bismuth (GEHC)
Rendre la vue à ceux qui l’ont perdue a longtemps été considéré comme un sujet réservé à la science-fiction. Cependant,
sur les vingt dernières années les efforts intensifiés dans le domaine des prothèses visuelles ont abouti à des avancées
significatives, et plusieurs centaines de patients dans le monde ont reçu de tels dispositifs. Ce séminaire présentera
brièvement le domaine des prothèses rétiniennes avec une focalisation particulière sur les aspects de traitement
d’image. Nous exposerons les principales approches, les limitations connues et les résultats.
Vincent Bismuth mène une carrière dans le domaine du traitement d’image pour les dispositifs médicaux. Il a contribué
pendant plus de dix ans au développement d’algorithmes de traitement d’image et de vidéos pour les procédures
chirurgicales interventionnelles chez GE Healthcare. Il s’est ensuite consacré pendant quatre ans à la conception de
systèmes de restauration visuelle pour les malvoyants dans la start-up Pixium Vision. Fin 2018, il a rejoint la division
mammographie de GE Healthcare où il mène des développements en traitement d’image.
Mercredi 10 avril 2019, 11h - 12h, Amphi 4
Deep Learning for Satellite Imagery: Semantic Segmentation, Non-Rigid Alignment, and Self-Denoising
Guillaume Charpiat (Équipe TAU, INRIA Saclay / LRI - Université Paris-Sud)
Neural networks have been producing impressive results in computer vision these last years, in image classification or
segmentation in particular. To be transferred to remote sensing, this tool needs adaptation to its specifics: large
images, many small objects per image, keeping high-resolution output, unreliable ground truth (usually
mis-registered). We will review the work done in our group for remote sensing semantic segmentation, explaining the
evolution of our neural net architecture design to face these challenges, and finally training a network to register
binary cadaster maps to RGB images while detecting new buildings if any, in a multi-scale approach. We will show in
particular that it is possible to train on noisy datasets, and to make predictions at an accuracy much better than the
variance of the original noise. To explain this phenomenon, we build theoretical tools to express input similarity from
the neural network point of view, and use them to quantify data redundancy and associated expected denoising effects.
If time permits, we might also present work on hurricane track forecast from reanalysis data (2-3D coverage of the
Earth's surface with temperature/pressure/etc. fields) using deep learning.
After a PhD thesis at ENS on shape statistics for image segmentation, and a year in Bernhard Schölkopf's team at MPI
Tübingen on kernel methods for medical imaging, Guillaume Charpiat joined INRIA Sophia-Antipolis to work on computer
vision, and later INRIA Saclay to work on machine learning. Lately, he has been focusing on deep learning, with in
particular remote sensing imagery as an application field.
https://www.lri.fr/~gcharpia/
Mardi 1 octobre 2019, 11h - 12h, Amphi 4
The Loci Auto-Parallelizing Framework: An Overview and Future Directions
Edward A. Luke, Professor, Department of Computer Science and Engineering, Mississippi State University
The Loci Auto-Parallelizing framework provides a Domain Specific
Language (DSL) for the creation of high performance numerical
models. The framework uses a logic-relation model to describe
irregular computations, provide guarantees of internal logical
consistency, and provides for automatic parallel execution. The
framework has been used to develop a number of advance computational
models used in production engineering processes. Currently Loci based
tools form the backbone of computational fluid dynamics tools used by
NASA Marshall and Loci based codes account for more than 20% of the
computational workload on NASA’s Pleiades supercomputer. This talk
will provide an overview of the framework, discuss its general
approach, and provide comparisons to other programming models through
a mini-app benchmark. In addition, future plans for developing
efficient schedules of fine-grained parallel and memory bandwidth
constrained computations will be discussed. Finally, some examples of
the range of engineering simulations enabled by the technology will be
introduced and briefly discussed.
Dr. Ed Luke is a professor of computer science in the computer science
department of Mississippi State University. He received his Ph.D. in
the field of Computational Engineering in 1999 and conducts research
at the intersection between applied math, computer science. His
research focuses on creating systems to automatically parallelize
numerical algorithms, particularly those used to solve systems of
partial differential equations. Currently Dr. Luke is participating
in active collaborations with INRIA in Paris conducting research in the
areas of solver parallelization and mesh generation.
http://web.cse.msstate.edu/~luke/loci/index.html
Mardi 17 décembre 2019, 10h - 11h, IP12A
Learning the relationship between neighboring pixels for some vision tasks
Yongchao Xu, Associate Professor at the School of Electronic Information and Communications, HUST, China
The relationship between neighboring pixels plays an important role in many vision applications. A typical example of a relationship between neighboring pixels is the intensity order, which gives rise to some morphological tree-based image representations (e.g., Min/Max tree and tree of shapes). These trees have been shown useful for many applications, ranging from image filtering to object detection and segmentation. Yet, these intensity order based trees do not always perform well for analyzing complex natural images. The success of deep learning in many vision tasks motivates us to resort to convolutional neural networks (CNNs) for learning such a relationship instead of relying on the simple intensity order. As a starting point, we propose the flux or direction field representation that encodes the relationship between neighboring pixels. We then leverage CNNs to learn such a representation and develop some customized post-processings for several vision tasks, such as symmetry detection, scene text detection, generic image segmentation, and crowd counting by localization. This talk is based on [1] and [2], as well as extension of those previous works that are currently under review.
[1] Xu, Y., Wang, Y., Zhou, W., Wang, Y., Yang, Z. and Bai, X.,
2019. Textfield: Learning a deep direction field for irregular scene
text detection. IEEE Transactions on Image Processing.
[2] Wang, Y., Xu, Y., Tsogkas, S., Bai, X., Dickinson, S. and Siddiqi,
K., 2019. DeepFlux for Skeletons in the Wild. In Proceedings of the
IEEE Conference on Computer Vision and Pattern Recognition.
Yongchao Xu received in 2010 both the engineer degree in electronics & embedded systems at Polytech Paris Sud and the master degree in signal processing & image processing at Université Paris Sud, and the Ph.D. degree in image processing and mathematical morphology at Université Paris Est in 2013. After completing his Ph.D. study at LRDE, EPITA, ESIEE Paris, and LIGM, He worked at LRDE as an assistant professor (Maître de Conférences). He is currently an Associate Professor at the School of Electronic Information and Communications, HUST. His research interests include mathematical morphology, image segmentation, medical image analysis, and deep learning.
http://www.vlrlab.net/~yxu/
Mercredi 12 février 2020, 10h - 11h30, Amphi 1
Informatique Quantique
Georges Uzbelger, IBM France
Dans ce séminaire, nous parlerons d'une technologie émergente qu'est l'informatique quantique, exploitant les phénomènes quantiques de l'infiniment petit. Nous verrons que, quand dans le monde de l'informatique classique, les données sont représentées par des bits valant chacun 0 ou 1 exclusivement, alors que l'informatique quantique est déroutante dans le sens où les qubits (bits quantiques) peuvent valoir simultanément 0 et 1. Afin de pouvoir appréhender cette technologie, nous rappellerons ce que sont la dualité onde/corpuscule, la superposition d'états, ainsi que intrication quantique. Nous verrons aussi comment IBM a créé le premier processeur quantique (ou QPU) quelques dizaines d'années après l'idée révolutionnaire du père de l'informatique quantique, Richard Feynman, et quels sont les défis technologiques qui en découlent. Nous verrons que l’informatique quantique offre de nouvelles perspectives dans les domaines comme la cryptographie et l'intelligence artificielle pour ne citer qu'eux. Une étude des complexités des différents algorithmes vus durant le séminaire sera évoqué. Durant cette plénière interactive, une démonstration sera réalisée via l’environnement de développement Qiskit avec accès à distance à une machine quantique IBM. Merci donc d'apporter votre ordinateur portable !
Diplômé de l’Université Paris IX Dauphine en Mathématiques et Applications Fondamentales, Georges Uzbelger est depuis 2002 ingénieur chez IBM France, en charge actuellement de prestations de consulting et de design de solutions dans le domaine de l’IA, de l’advance analytics et de l’informatique quantique. Il participe au programme IBM Quantum Experience pour le développement de l’informatique quantique et notamment du calcul et de l’algorithmique quantique. Adhérent à la SMF (Société Mathématique de France) entre autre, il enseigne également à l’Ecole Polytechnique, à Sorbonne Université (UPMC) et à l’Université Paris-Dauphine.
http://www.research.ibm.com/quantum/
Mercredi 18 mars 2020, 11h - 12h, Amphi Masters
Diagnosis and Opacity in Partially Observable Systems
Stefan Schwoon, ENS Paris-Saclay
In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems
when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz.
Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) at Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems.
http://www.lsv.fr/~schwoon/
Mercredi 16 décembre 2020, 11h - 12h, {\small https://eu.bbcollab.com/collab/ui/session/guest/95a72a9dc7b0405c8c281ea3157e9637}
Diagnosis and Opacity in Partially Observable Systems
Stefan Schwoon, ENS Paris-Saclay
In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems
when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz.
Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) at Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems.
http://www.lsv.fr/~schwoon/
Mercredi 10 février 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE
Generating Posets Beyond N
Uli Fahrenberg, Ecole Polytechnique
We introduce iposets - posets with interfaces - equipped with a novel gluing
composition along interfaces and the standard parallel composition. We study
their basic algebraic properties as well as the hierarchy of gluing-parallel
posets generated from singletons by finitary applications of the two
compositions. We show that not only series-parallel posets, but also
interval orders, which seem more interesting for modeling concurrent and
distributed systems, can be generated, but not all posets. Generating posets
is also important for constructing free algebras for concurrent semi-rings
and Kleene algebras that allow compositional reasoning about such systems.
Ulrich (Uli) Fahrenberg holds a PhD in mathematics from Aalborg University, Denmark. He has started his career in computer science as an assistant professor at Aalborg University. Afterwards he has worked as a postdoc at Inria Rennes, France, and since 2016 he is a researcher at the computer science lab at École polytechnique in Palaiseau, France. Uli Fahrenberg works in algebraic topology, concurrency theory, real-time verification, and general quantitative verification. He has published more than 80 papers in computer science and mathematics. He has been a member of numerous program committees, and since 2016 he is a reviewer for AMS Mathematical Reviews.
http://www.lix.polytechnique.fr/~uli/bio.html
Mercredi 31 mars 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Amphi 4
Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems
Souheib Baarir, Université Paris VI
Despite its NP-completeness, propositional Boolean satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts like planning decision, cryptology, computational biology, hardware and software analysis. Hence, the development of approaches allowing to handle increasingly challenging SAT problems has become a major focus: during the past eight years, SAT solving has been the main subject of my research work. This talk presents some of the main results we obtained in the field.
Souheib Baarir est Docteur en informatique de l'Université de Paris VI depuis 2007 et a obtenu son HDR à Sorbonne Université en 2019. Le thème de ses recherches s'inscrit dans le cadre des méthodes formelles de vérification des systèmes concurrents. En particulier, il s’intéresse aux méthodes permettant d’optimiser la vérification en exploitant le parallélisme et/ou les propriétés de symétries apparaissant dans de tels systèmes.
https://www.lip6.fr/actualite/personnes-fiche.php?ident=P617
Mercredi 12 mai 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE
An Introduction to Topological Data Analysis with the Topology ToolKit
Julien Tierny, Sorbonne Université
Topological Data Analysis (TDA) is a recent area of computer science that focuses on discovering intrinsic structures hidden in data. Based on solid mathematical tools such as Morse theory and Persistent Homology, TDA enables the robust extraction of the main features of a data set into stable, concise, and multi-scale descriptors that facilitate data analysis and visualization. In this talk, I will give an intuitive overview of the main tools used in TDA (persistence diagrams, Reeb graphs, Morse-Smale complexes, etc.) with applications to concrete use cases in computational fluid dynamics, medical imaging, quantum chemistry, and climate modeling. This talk will be illustrated with results produced with the "Topology ToolKit" (TTK), an open-source library (BSD license) that we develop with collaborators to showcase our research. Tutorials for re-producing these experiments are available on the TTK website.
Julien Tierny received his Ph.D. degree in Computer Science from the University of Lille in 2008 and
the Habilitation degree (HDR) from Sorbonne University in 2016. Currently a CNRS permanent
research scientist affiliated with Sorbonne University, his research expertise lies in topological methods
for data analysis and visualization. Author on the topic and award winner for his research, he regularly
serves as an international program committee member for the top venues in data visualization (IEEE VIS,
EuroVis, etc.) and is an associate editor for IEEE Transactions on Visualization and Computer Graphics.
Julien Tierny is also founder and lead developer of the Topology ToolKit (TTK), an open source library for
topological data analysis.
https://topology-tool-kit.github.io/
Mercredi 6 octobre 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Salle IP 13
Scaling Optimal Transport for High Dimensional Learning
Gabriel Peyré, CNRS and Ecole Normale Supérieure
Optimal transport (OT) has recently gained a lot of interest in machine learning. It is a natural tool to compare in a geometrically faithful way probability distributions. It finds applications in both supervised learning (using geometric loss functions) and unsupervised learning (to perform generative model fitting). OT is however plagued by the curse of dimensionality, since it might require a number of samples which grows exponentially with the dimension. In this talk, I will review entropic regularization methods which define geometric loss functions approximating OT with a better sample complexity.
Gabriel Peyré is a CNRS senior researcher and professor at Ecole Normale Supérieure, Paris. He works at the interface between applied mathematics, imaging and machine learning. He obtained 2 ERC grants (Starting in 2010 and Consolidator in 2017), the Blaise Pascal prize from the French academy of sciences in 2017, the Magenes Prize from the Italian Mathematical Union in 2019 and the silver medal from CNRS in 2021. He is invited speaker at the European Congress for Mathematics in 2020. He is the deputy director of the Prairie Institute for artificial intelligence, the director of the ENS center for data science and the former director of the GdR CNRS MIA. He is the head of the ELLIS (European Lab for Learning & Intelligent Systems) Paris Unit. He is engaged in reproducible research and code education.
https://optimaltransport.github.io/, http://www.numerical-tours.com/, https://ellis-paris.github.io/
Mercredi 22 juin 2022, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Salle KB000
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems
- Documents
- slides_Stan.pdf
Daniel Stan, Technische Universität Kaiserslautern
We present a framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In this framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. As in other regular model checking (RMC) techniques, a finite-state automaton is used to specify a parameterized family of systems.
Parameterized systems might also require an arbitrary number of announcements, leading to the introduction of the so-called iterated public announcement. Although model checking becomes undecidable because of this operator, we provide a semi-decision procedure based on Angluin's L*-algorithm for learning finite automata. Moreover, the procedure is guaranteed to terminate when some regularity properties are met. We illustrate the approach on the Muddy Children puzzle, and we further discuss dynamic protocol encodings through the Dining Cryptographer example.
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas
Since October 2019, Daniel Stan is a PostDoc in the Automated Reasoning group.
He was previously a PhD student (2013-2017) at LSV, ENS Paris Saclay under the
supervision of Patricia Bouyer and Nicolas Markey, then a PostDoc in the
Dependable Systems and Software chair of Saarbrücken. His research interests
include formal methods and model checking techniques with a particular focus on
Regular Model Checking and Automatic Structures, Parameterized Systems,
Stochastic Systems and Games. In particular, his current work put an emphasis on
exact learning algorithms with applications to model checking.
https://arg.cs.uni-kl.de/gruppe/stan/