Semantic search

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

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/

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.

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 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/

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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 13 mai 2015, 11h00-12h30, Salle L0 du LRDE

Programmation web haute performance avec C++14

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 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

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.

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 18 février 2015, 11h00-12h30, Salle L0 du LRDE

Faveod, meta-modèle au service de la qualité logicielle

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 17 décembre 2014, 11h00-12h00, Salle L0 du LRDE

D’un MOOC à l'autre

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 10 décembre 2014, 11h00-12h00, Salle L0 du LRDE

Une nouvelle approche pour la gestion de la mémoire avec CUDA

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 19 novembre 2014, 11h30-13h, Amphi 1

Generic Tools, Specific Languages

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 11 juin 2014, 14h30-16h, Salle L0, LRDE

Méthodes rapides pour le traitement, l'analyse et la synthèse en informatique graphique

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 14 mai 2014, 11h-12h30, Salle L0, LRDE

Nife : du Forth pour l'embarqué

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 12 mars 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

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

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 février 2014, 11h-12h30, Salle L0 du LRDE

Automates Acycliques

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/

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 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 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 13 novembre 2013, 11h-12h30, Salle Lα du LRDE

Address & Thread Sanitizer dans GCC: État Actuel et Orientation Future

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 9 octobre 2013, 11h-12h, Salle Lα du LRDE

GNU epsilon, un langage de programmation extensible

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 29 mai 2013, 10-12h, Salle Lα du LRDE

Langages de développement et sécurité - Mind your language

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 22 mai 2013, 11-12h, Salle Lα du LRDE

Étendre le compilateur GCC avec MELT

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 24 avril 2013, 11-12h, Salle L-Alpha du LRDE

Designing robust distributed systems with weakly interacting feedback structures

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 27 mars 2013, 11-12h, Salle L-Alpha du LRDE

SMIL : Simple Morphological Image Library

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 20 février 2013, 11-12h, Salle L-Alpha du LRDE

Une représentation d'images 2D discrète, continue et auto-duale

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 23 janvier 2013, 11h-12h, Salle L-Alpha du LRDE

Amélioration du design et des performances des machines virtuelles langages

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 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

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

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 4 juillet 2012, 14h00-16h30, Amphi 4

Vérification efficace de propriétés insensibles au bégaiement.

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

É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

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.