Talk abstract
From LRDE
This is a property of type Text.
S
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.
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… +
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.
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. +
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. +
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. +
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. +
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. +
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. +
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. +, 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. +
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. +
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...). +
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. +
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). +
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. +
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. +, 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. +
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. +
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. +
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. +
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. +