Abstract
From LRDE
.
La vérification de modèle vise à vérifier qu'un système répond à la spécification donnée en explorant tous ses états possibles. Pour y parvenir, il existe plusieurs techniques. Le Multi-Core Nested Depth-First Search (CNDFS) a un faible besoin en mémoire et fonctionne bien avec les automates de Büchi les plus simples. La Multi-Core On-The-Fly SCC Decomposition (UFSCC) a un besoin en m'moire plus important et fonctionne bien avec les automates de Büchi généralisés. La méthode symbolique a un besoin en mémoire plus faible mais dépend beaucoup de l'ordre des variables. Les performances de ces algorithmes peuvent être très différentes et choisir le meilleur en fonction d'un modèle spécifique sans les tester tous n'est pas quelque chose de facile. Ici, nous essayons d'utiliser de l'apprentissage automatisé pour prédire la meilleure méthode à utiliser pour un modèle donné. Pour celanous entraînons une forêt aléatoire, une méthode d'apprentissage d'ensemble qui utilise une multitude d'arbres de décision, en utilisant seulement les premiers états de l'espace d'état. +
... Insert an abstract in French here ... +
A
Spot is an extensible model checking library using transition-based generalized Büchi automata (TGBA). It contains many state-of-the-art algorithms. In this paperwe focus on two algorithms that create automata with more transitions than necessary. These constructions can be enhanced by computing a feedback arc set (FAS): a set of edges which, when removed from the graph, leave a directed acyclic graph. Ideally, we want a minimal FAS, but this problem is NP-hard. We adapted and improved a heuristic proposed by Eades et al. that approximates a minimal FAS in linear time. We show that the integration of this heuristic in the complementation of deterministic Büchi automata and in the conversion of Rabind automata to Büchi automata reduces the size of the output up to 31% in our experiments. These results depend greatly on the number of cycles and accepting states in the input automaton. +
Spot is a C++ library for model checking. For verification, Spot uses an input-format which describes a Transition-based Generalized Büchi Automata (TGBA). However, this format doesn't seem accessible for users with its poor abstraction and the need for often representing automaton with millions of states. Promela (Process Meta-Language) is a verification modeling language used by the Spin model checker. It lets users to describe a parallel system for verification in a high level programming language. We will present different ways to add a Promela front-end in Spot, which will allow to explore the state-graph on-the-fly, in order to avoid storing all the states. +
Thanks to the HOA format there are less and less barriers between '"`UNIQ--math-00000005-QINU`"'-automata with different acceptance conditions. Spot, a library for '"`UNIQ--math-00000006-QINU`"'-automata manipulation, supports arbitrary acceptance condition and performs some conversions between them. We augmented the set of supported acceptance conversions with new algorithms that convert (when possible) all common classes of non deterministic '"`UNIQ--math-00000007-QINU`"'-automata to deterministic co-Büchi. Boker and Kupferman solved this conversion whith asymptotically tight constructions. We implement their methods with some optimizations and adjustments: we made it work with Streett-like acceptance, any acceptance in disjunctive normal form (including Rabin-like) and also transition-based acceptance. Using these conversions gives a new way to check whether an LTL formula is a persistence formula. +
Image recognition main objective is to enable computers to recognize shapes without needing any human intervention. However, one problem in this field is automatic recognition regardless to image transformations like rotation or scales changes. Image invariants based on moments have received a particular attention since they respect fully or partially the constraints listed above. Various shape-based invariant algorithms are popular in Document Image Analysis and especially for Optical Character Recognition systems since they provide relevant features used to differentiate characters. Nevertheless, they also find an interesting application in Document Layout Analysis by providing information that can be used to distinguish text from non-text elements. Thus, we will introduce the concepts of image invariants and evaluate the performances of six state-of-the-art shape-based image invariants for text / non-text classification. An attempt of an image invariant algorithm inspired from the principle of compressive sensing is also offered. +
For the last few years, connected operators have gained a certain popularity in image processing field, they have been widely used for filtering, image segmentation, object detection...However, they encountered several issuesthe most important being contrast dependence, one can only retrieve either dark or bright objects. Auto-dual operators allow computation on dark and bright components in the same time and as a consequence, do not suffer from the drawback of classical connected operators. Howeverauto-dual operators are more difficult to implement and current algorithms are computationally expensive. We propose a new algorithm to compute auto-dual operators based on Tarjan's union-find which is faster that current state-of-the-art contour tree algorithms. +
Spot is a model checking library centered around the automata-theoretic approach, and can be used to verify properties expressed using LTL (Linear Temporal Logic) formulæ on models represented as TGBA (Transition-based Generalized Büchi automata). The library offers three algorithms to translate LTL formulæ to TGBA, one of the main stages of the approach. We present a forth translation algorithm introduced by Tauriainen which uses TAA (Transition-based Alternating Automata) as an intermediate representation. We also compare it to the three algorithms already present in Spot. +
The Tree of Shapes is an useful image transform used to process digital images in a self-dual way. We recently introduced a new algorithm to compute this tree in '"`UNIQ--math-00000005-QINU`"'-dimensional gray scale images with a quasi-linear time complexity. However, no proof nor benchmark were given. In addition, this algorithm requires to increase dramatically the size of the input image. Such increase comes with an important cost in term of memory usage and computation times. We discuss the initialization of the algorithm and provide a proof. We also address its memory and computation time issues when used on two dimensional images. +
This report focuses on an active learning algorithm for the class of visibly one-counter automata,and its implementation in python and C++. The algorithm allows creating such automata using queriesto a teacher, with no knowledge on the final automaton. We then discuss the possible improvements of the algorithm regarding the algorithm execution speed and the automaton represention. We also give an overview of how benchmarks could be perform on such a semi-automatic program. +
Vaucanson est une bibliothèque C++ de manipulation d'automates finis. Le feedback utilisateur montre que Vaucanson est lent et que l'interface de la bibliothèque qui permet de manipuler les automates directement est complexe. Pour améliorer Vaucanson, l'équipe de développement met en place une interface simplifiée sur la structure de données Automata et réinstaure une modélisation saine de l'implémentation sous-jacente. Une conséquence de ces changements est que les algorithmes disponibles dans Vaucanson doivent être adaptés à la nouvelle interface. L'adaptation de ces algorithmes donne l'opportunité d'étudier l'impact des changements récents sur les performances et l'accessibilité de Vaucanson. Grâce à la simplicité de la nouvelle interface, les optimisations possibles deviennent plus visibles. +
Le principe d'un algorithme de ligne de partage des eaux est de partionner en régions (bassins) une image en niveaux de gris. Plus particulièrement, l'algorithme de "watershed cut" opère des coupes dans un graphe formé à partir d'une image et dont les arêtes sont valuées. Une premiére approche a été de considérer l'image comme un graphe 4-connexe dont les sommets sont les pixels. Il est alors apparu que cette approche pouvait masquer des minima locaux. Une seconde solution, à base de complexe simplicial, a donc été étudiée. Ce travail de recherche utilise la bibliothèque Milena, la bibliothèque générique de traitement d'images en C++ développée au laboratoire. +
The main purpose of the watershed algorithm is to segment a gray-level image into regions (basins). More specifically, the "watershed cut" algorithm performs some cuts in an edge-valued graph built from an image.First we have considered an image as a 4-connected graph, where the vertices represent the pixels. Yet we have noticed that this representation can miss some local minima. A second approach, based on a simplicial complex, has been studied. This work relies on Milena, the generic C++ library dedicated to image processing library developed at the LRDE. +
La conception des automates dans Vaucanson occupe une place centrale concernant la généricité de la bibliothèque. Nous voulons pouvoir étendre cette modélisation pour supporter de nouveaux types et spécialiser des comportements afin d'améliorer les performances. L'introduction récente du concept de kind à la bibliothèque ainsi que la définition d'une nouvelle interface des automates ont pour objectifs de rationaliser les structures de données déjà présentes dans Vaucanson, comme les graphes utilisant Boost Multi Index. Le kind d'un automate est le type d'étiquettes qu'il porte sur ses transitions, une lettre ou un mot par exemple. L'utilisateur peut alors, à travers une hiérarchie d'itérateurs respectant la nouvelle interface, itérer de manière efficace sur les transitions portant une occurrence de ce kind spécifié comme prédicat (itérer sur les transitions portant la lettre a par exemple). Le gain est visible car l'utilisateur était contraint d'itérer sur le support d'un polynôme avant ces améliorations. +
Vaucanson is an extensive C++ library for the manipulation of finite state machines. User feedback shows that Vaucanson is slow and that the library interface for direct automaton manipulation is complex. To enhance Vaucansonthe development team is making major changes to simplify the interface over the Automata data structure and reinstate a sane modeling for the underlying implementation. A consequence of these changes is that the algorithms available in the Vaucanson library must be adapted to the new interface. Adapting algorithms is an opportunity to study the impact of the recent interface and implementation changes on performance and accessibility. Because the new interface over automata is simplerpossible optimizations are more apparent. +
The design of automata in Vaucanson plays a central role concerning the genericity of the library. We want to be able to extend the model to support new types and to specialize behaviours in order to improve performances. The recent introduction of the kind concept in the library together with the definition of a new automata interfaceare targeting the rationalisation of already existing data structures in Vaucanson — Boost Multi Index based graphs for example. The kind of an automaton is the type of the labels on the transitions like a letter or a word. Through an iterator hierarchy respecting the new interface, the user can efficiently iterate over the transitions labeled by a specific occurrence of the kind specified by a predicate — iterating over all the transitions labeled by an '"`UNIQ--math-00000005-QINU`"' for example. The gain is noticeable because the user had no choices but to iterate over a polynomial before those improvements. +
Explicit model checking of concurrent systems suffers from the exponential blow-up in the number of states of the represented system. The partial order reduction methods are a set of methods to tackle this problem. They act by preventing the generation of redundant states while creating the state space. Among all these methods are the two phase and ample set algorithms that serve as the basis for our investigations. We implemented those algorithms in Spot, the C++, model-checking library developed at the LRDE, using the Divine interface. Building on these classical methods and taking advantadge of the on-the-fly property of Spot's algorithms, it is possible to devise a new class of methods called adaptive partial order methods that use the current state of the formula automaton and not the whole formula. This new method gives better results than the classical partial order methods on our test suite. +
Contract programming is a paradigm that allows developers to ensure that some conditions are satisfied when a function is called (preconditions), or when it returns (postconditions). It makes debugging easier and it is a good way to document what a function accepts as argument or ensures on the result. In oriented-object languages, it is also possible to check a set of conditions on every call and return of any member function of a class (class invariants), and conditions are inherited from parent classes. The Transformers project aims at providing source to source transformations on C and C++ sources. A C extension to support contracts in C has already been written, when C++ parsing wasn't working yet. We will show how to write a C++ grammar extension to bring contracts in the C++ with the Transformers project, and then how to transform this extended C++ into standard C++. +
La programmation par contrats est un paradigme permettant de réduire le temps de débogage des programmes, en spécifiant des conditions qui doivent être vérifiées à l'entrée d'une fonction (emph préconditions) ou à sa sortie (emph postconditions). Dans les languages orientés objet, il est également possible de vérifier un ensemble de contraintes à chaque appel ou sortie d'une fonction membre (invariants de classe), et les conditions sont héritées à partir des classes parentes. Le projet Transformers a pour but de faire de la transformation source à source sur des sources C et C++. Une extension pour introduire les contrats dans le C a déjà été écrite alors que l'analyse syntaxique du C++ n'était pas encore fonctionnelle. Nous allons montrer comment écrire une extension de la grammaire du C++ dans le projet Transformers pour introduire le principe de contrat dans le C++, puis transformer le code étendu en C++ standard. +
Les transducteurs sont utilisés dans beaucoup de contextes, comme la reconnaissance de parole ou le calcul de la similitude entre proteines. Cette recherche montre l'implémentation dans Vcsn de plusieurs algorithmes permettant de manipuler des transducteurs afin de résoudre ces problèmes. Tout d'abord, un algorithme permettant de transformer un transducteur en automate pondéré qui peut être facilement évalué est présenté. L'algorithme de synchronisation a ensuite été implémenté, ce qui a amené au calcul du transducteur des distances d'édition, et son évaluation. +
Transducers are used in many contexts, such as speech recognition or in order to measure the similarity between proteins. This research shows the implementation in Vcsn of several algorithms allowing to manipulate the transducersand thus solve these problems. First an algorithm to transform a transducer into a weighted automaton that can be easily evaluated is presented. The synchronization algorithm was then implemented, leading to the computation of the edit-distance transducer and its evaluation. +
Nash equilibria computation in finite games is a problem which is known to be PPAD-complete, which means it currently seems impossible to find an efficient solution ; worst case complexity of well known algorithms is in '"`UNIQ--math-00000007-QINU`"' for any game of size '"`UNIQ--math-00000008-QINU`"'. For this reasonresearch in this domain currently focuses on '"`UNIQ--math-00000009-QINU`"'-equilibria, situations which approximately satisfy the conditions of a Nash equilibrium. The emphFictitious Play algorithm fits in this approach. At each iteration of this algorithm, each of the players “strengthens” the strategy that has the highest utility in the current context. For some specific game classes this algorithm converges to a Nash equilibrium, therefore providing an efficient approximation method. However, convergence can only be proved for a small amount of game classes. It is therefore useful to study other algorithms (based on Fictitious Play) in order to find other convergence cases. In this study, we will focus on the alternate Fictitious Play algorithm, in which only one player at a time strengthens one of his strategies : the player which is the “further” from his maximum payoff. +
Alternating automata add a universal branching to the existential branching from non-deterministic automata. Büchi alternating automata are exponentially more concise than non-deterministic Büchi automata. Additionally, they are well suited to translate linear temporal logic as their size is proportional to the translated formula. This work aims to add alternating automata support to Spot. This will make Spot compatible with other tools producing or using aternating automata, and allow future algorithms working on alternating automata to be implemented. +
Une des parties d'une chaîne de reconnaissance de caractères est la classification des caractères à proprement parler : ils peuvent être en majusculesminuscules ou bien être des chiffres. Dans notre casnotre OCR calcule un descripteur à base d'ondelettes pour chacune des images de caractère. Ce sont ces descripteurs que nous classifions. L'étape de classification est actuellement basée sur un algorithme des k plus proches voisins (k-NN) multi-classe. Sachant que l'étape d'évaluation dépend fortement de la taille de la base d'entraînement, cette dernière peut être modifiée afin d'améliorer les scores. Notre travail se concentre sur ces possibles améliorations de la base d'entraînement. vspace*1.05cm +
Vaucanson est une bibliothèque dont un des buts est de permettre un accès facilité à des automates et aux algorithmes qui leur sont associés. Elle met donc à notre disposition plusieurs algorithmes standard (et d'autres moins conventionnels) tels que la déterminisation, le calcul des états accessibles etc. L'un de ces algorithmes est la composition de transducteurs. Celui-ci n'est pas d'une nature aisée à aborder et son implémentation dans Vaucanson est perfectible. Améliorer l'implémentation d'un tel algorithme est alors un bon moyen de mettre à l'épreuve certains choix de conception dans Vaucanson. +
Spot est une bibliothèque de model checking developée au LRDE. Sa force est d'utiliser les Automates de Büchi Generalisés basés sur les transitions (TGBA), plutôt que les Automates de Büchi basés sur les Transitions (TBA) très utilisés dans les autres model checkers. Les TGBA nous permettent de produire des automates très petits représentant une formule rendant toutes les étapes suivantes du model checking plus rapide. Comme Spot met l'accent sur l'utilisabilité et la personnalisation des outils, une attention particulière est portée sur l'interfaçage avec d'autres programmes. La question de transformer un TGBA en TBA (appelé dégeneralization) sans perdre en performance est donc centrale. Cette présentation a pour but de montrer une analyse des outils de dégénéralisation présents dans Spot et de proposer des moyens pour les améliorer. +
En vérification formelle à l'aide d'ω-automates, la construction d'automates plus petits réduit beaucoup le temps d'exécution et la consommation mémoire d'opérations coûteuses telles que le produit synchronisé. La minimisation d'ω-automates étant un problème NP-complet, nous concentrons notre travail sur les opérations de réduction. Spot possède déjà une méthode de réduction par simulation fonctionnant pour tous les automates existentiels ayant n'importe quelle condition d'acceptation. Cette méthode utilise une simulation à un pas reposant sur la signature des états. L. Clemente et R. Mayr proposent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l'augmentation de ce nombre de pas peut améliorer la réduction. Nous essayons une généralisation de l'opération de réduction existante dans Spot pour qu'elle fonctionne avec des simulations à n pas reposant sur la signature des états. Nous présentons également comment étendre la réduction existante afin qu'elle fonctionne également pour les automates alternants. +
Calculer le flux optique a de nombreuses applications telles que l'estimation de mouvement ou un premier pas vers l'inpainting vidéo. L'équation du flux optique ne peut pas être résolue telle quelle à cause du problème de fenêtrage (deux inconnues pour une seule équation). Un ensemble d'algorithme essaie de résoudre cette équation en se basant sur une stratégie globalec'est-à-dire en essayant d'avoir des petites variations dans le flux. Le premier d'entre eux est l'algorithme d'Horn-Schunck. Celui-ci, même s'il marche dans de nombreux cas, a plusieurs inconvénients, y compris celui d'être lent et de ne pas pouvoir trouver les grands déplacements. Dans le but de résoudre ces problèmesplusieurs stratégies ont été développées. Nous présenterons la méthode et analyserons les bénéfices apportés en appliquant une stratégie multi-échelle à l'algorithme d'Horn-Schunck. +
Vaucanson 2 est une jeune plate-forme de manipulation d'automates née des cendres de Vaucanson. Ce redémarrage à zéro a été fortement encouragé par quelques problèmes de conception : difficultés à gérer trop de templates et trop de niveaux d'imbrication de ceux-ci, qui tendent à obfusquer le code quand les concepts templates ne sont pas clairement définis ; des limitations de performances due à une approche de "généralisation" ; etc. Vaucanson 2 entend apprendre des erreurs de son prédecesseur, et dans ce but, un vrai travail de conception doit être fait. Les templates doivent être utilisés pour la performance (évitant un usage abusif de fonctions virtuelles) afin de pouvoir préférer la généricité plutôt que la généralité, tout en conservant une flexibilité lors de l'exécution. Vaucanson 2 prétendra aussi à une compilation dynamique de code (types d'automates et algorithmes) et de le charger en tant que bibliothèque dynamique. Ces simples problèmes amènent à des architectures de distribution complexes et d'effacement de type, qui doivent être testés dans un environnement simulé. +
L'algorithme de Safra permet de construire des automates de Rabin déterministes à partir d'automates de Büchi non-déterministes. Il existe une variante à cette méthode qui permet de construire des automates à parités déterministes. Cependant, ces méthodes produisent des automates avec 2^O(nlogn) états. Il existe des améliorations qui permettent de réduire le nombre d'états dans beaucoup de cas. Nous présentons deux nouvelles stratégies pour aider à réduire le nombre d'états final. La première stratégie utilise les composantes fortement connexes et utilise cette information pour suivre des chemins de Safra différents. La deuxième stratégie utilise l'information retournée par la bisimulation pour retirer des états équivalents. Ceci permet d'éviter de parcourir plusieurs chemins équivalents et ainsi de réduire le nombre d'états final. On montre que nos stratégies permettent souvent de construire des automates déterministes avec moins d'états et que ces automates reconnaissent toujours le même language. On donne des benchmarks pour voir le gain apporté par nos stratégies et on utilise un outil appelé ltl2dstar qui produit des automates de Rabin déterministes à partir de formules LTL pour comparer nos résultats. +
We propose a new edge-based method dedicated to image segmentation. The last few years have shown the development of image processing with connected filters. Indeedcontour-preserving properties of connected operators are highly desired for image segmentation. The connected operators-based segmentation methods usually proceed in two steps. They first compute an attribute on the connected components and filter the components of which attribute do not satisfy a criterion. In these methods, attributes are actually computed on the pixels of connected components. We propose a new union-find based algorithm that enables evaluation of attributes on connected component edges so that we can finally compute an attribute on their contours. We therefore introduce edges-based attributes and propose some of them that evaluate a connected components energy. We finally perform an edge-based attribute filtering to produce a new image segmentation method. +
Probabilistic model checkers usually rely on deterministic automata as the uniqueness of each path simplifies the probabilistic calculation. Unfortunatelythere are not many LTL translators that produce deterministic automata. Moreover, the automata produced by Spot, a model checker library, are not always deterministic. A classical powerset construction cannot always determinize '"`UNIQ--math-00000003-QINU`"'-automata. However, by memorizing the accepting paths, Safra's construction is able to convert a nondeterministic Büchi automaton into a deterministic Rabin automaton. This change of acceptance condition is necessary as deterministic Büchi automata are less expressive than the nondeterministic version. By implementing this construction, Spot will be able to determinize any automata and compute its complement. In this report, we will see how to efficiently implement the Safra construction and how to expand it to also determinize transition-based generalized Büchi automata. +
SCOOL is a domain-specific language (DSL) designed to make high-level C++ development easier. Based on SCOOP, a paradigm mixing generic and object-oriented programming, it features static resolution of member function calls and powerful concept checking. Previously, a standard container library had been made in pure C++ using SCOOP. Howeverthis implementation required high control of the C++ techniques of SCOOP. With SCOOL, we can achieve this by leaving the hard work to the C++ translator. Focusing on the development of the library with SCOOL and the essential changes to the language and its compiler, we will compare the native and DSL solutions and assess that SCOOL is well-fitted for generic application prototyping. +
Cxx has achieved to support classic object-oriented and generic programming, but some modelisation problems remain recurrent and difficult to solve. Scoop is a static Object-Oriented paradigm. The paradigm provides virtual methods, argument covariance, virtual types and multi-methods statically typed without extending the language. Scoop uses its own Cxx library in order to make easier to design a library with this paradigm. +
FIXME +
FIXME +
L'extraction des différentes structures d'un document numérisé se base sur la mise en place d'une chaîne de traitements constituée d'un certain nombre d'étapes primordiales afin d'optimiser la qualité du rendu final. L'étude de la mise en page du document, à savoir la localisation des lignes de texte et des paragraphesconstitue le coeur même de la chaîne puisque le rendu obtenu est étroitement corrélé avec les zones de texte données en entrée à l'OCR. Ainsi, nous présenterons une méthode hybride d'analyse de mise en page développée dans le cadre du projet SCRIBO. +
Vaucanson est une bibliothèque C++ de manipulation d'automates finis. Par rapport à son concurrent principal, OpenFST, Vaucanson souffre d'importants problèmes de performances. Afin d'améliorer les performances de Vaucanson, il est nécessaire d'avoir des outils appropriés pour analyser le comportement de la bibliothèque en termes d'utilisation de temps CPU et de gestion de la mémoire. Jusqu'en Mars 2009, il n'existait pas d'outils de ce type pratiques à utiliser avec Vaucanson. CBS (C++ Benchmarking Suite) est une suite d'outils d'analyse de performances pour projets C++. Ces outils permettent de mesurer, d'afficher, et de comparer l'utilisation de ressources (temps, mémoire), dans un format accessible à l'utilisateur. Ils sont utilisés pour analyser Vaucanson afin de réécrire les algorithmes les moins efficaces. +
L'extraction de structures dans un document numérisé se base sur la mise en place d'une chaîne de traitements constituée de briques élémentaires. L'analyse haut-niveau d'un document nécessite des informations structurelles sur celui-ci et se basera donc sur cette chaîne de traitements. Elle consistera à extraire des informations plus abstraites de nature structurelle sur un document, pour obtenir des "indices" sur la structure du document. À l'aide de ces indices et de schémas de structure, il est ensuite possible de réaliser des traitements de haut-niveau tels que l'identification du flot de lecture, l'extraction d'éléments spécifiques ou la reconstruction d'un document dans un autre format. +
La segmentation d'image est le processus d'identification du contour des objets qui composent une image. Ces dernières années, l'utilisation de Réseaux Neuronaux Convolutionnels Profonds à des fins de segmentation d'image a fortement augmenté, avec des résultats supérieurs à ceux d'approches plus classiques. Nous explorerons l'implémentation et les applications potentielles des filtres de la théorie de la Morphologie Mathématique dans la structure d'un Réseau Neuronal Convolutionnel Profond. +
Ce travail applique les réseaux de neurones artificiels à convolution (CNN) à la reconnaissance du locuteur. Le CNN est utilisé pour approximer une mesure de la distance entre deux i-vectors (vecteurs représentant les composantes de la voix d'une personne). Contrairement à la distance cosinus, fréquemment utilisée comme mesure de distance entre deux vecteurs, la fonction approximée par un CNN peut être non-linéaire. La performance de ce modèle sera comparée à celles de la distance cosinus et du classificateur PLDA. +
Olena est l'une des bibliothèques de traitement d'images dont la généricité est la plus poussée. Celle-ci vient principalement d'une vision différente de la notion d'image via des concepts clés tels que les fenêtresaccumulateurs, dispatch par traits ainsi que les morphers. On va s'attacher à en faire une description détaillée ainsi que montrer comment les implémenter en Lisp. +
L'arbre des formes est une transformée d'image utile pour effectuer des traitements sur des images discrètes de façon auto-duale. Un algorithme (non publié)travaillant sur des images n-dimensionnelles dans l'espace des complexes cellulaires, nous permet déjà de construire un arbre des formes en temps quasi-linéaire. Cependant, cet algorithme reste souvent largement plus lent que d'autres approches en temps theta(nlog(n)) sur des images naturelles en 2D ou 3D, le nombre de cellules à traiter dans l'espace des complexes étant très élevé. En vue d'améliorer ces temps de calculs, nous présentons une approche pour paralléliser l'algorithme de calcul d'arbre quasi-linéaire en exhibant des propriétés topologiques et algorithmiques qui ne peuvent être facilement obtenues par les autres approches existantes. +
Approximation de la distance entre i-vecteurs par Perceptron Multi-Couches dans les systèmes de reconnaissance du locuteur +
Actuellement, l'espace des i-vecteurs est la représentation standard des paramètres de la parole dans les systèmes de reconnaissance du locuteur. Le calcul du score est généralement basé sur la distance cosinus, ou sur l'analyse discriminante linéaire probabiliste. Le but de ce sujet est de remplacer ces approches par un Perceptron Multi-Couches (PMC). Le PMC a montré en effet de bonnes performances pour approximer des fonctions non linéaires. L'idée principale étant de trouver une meilleure fonction que la distance cosinus. Les performances du perceptron multi-couches seront comparées aux autres méthodes comme la distance cosinus, l'analyse linéaire discriminante probabilisteou encore la machine de Boltzmann restreinte qui sera présenté par Jean Luc. +
Ce rapport se concentre sur l'explication d'un algorithme d'apprentissage actif sur la classe des automates visiblement á un compteur, et son implémentation en python et C++. L'algorithme en lui meme permet de créer ce type d'automates en disposant seulement d'un professeursans connaitre l'automate d'arrivée. Nous discutons ensuite des améliorations possibles de l'algorithme concernant sa vitesse d'execution et la représentation d'un automate. Nous donnons aussi une idée de comment est-ce qu'un tel programme semi-automatique peut etre évalué par un benchmark. +
Climb est une bibliothèque de traitement d'images générique ayant pour objectif le prototypage rapide. L'implémentation de deux algorithmes d'arbre de composantes impacte Climb de plusieurs façons : la définition des valeurs est étendue, de nouveaux ensembles de sites sont ajoutés et les outils de développement sont améliorés. Un détour est pris afin de comprendre le patron de conception de chaînage popularisé par la bibliothèque jQuery. La méthode est modifiée afin de s'adapter au traitement d'images ainsi qu'à Common Lisp. Elle est également étendue via une notation parallèle ainsi qu'avec une meilleure gestion du fil d'exécution. +
The objective is to improve Spot, a model checking library. Spot deals with a specific kind of graph in which each state is a set of variables with given values. These values can be seen as coordinates and a state can therefore be seen as a N-dimensional point. The state space is then a N-dimensional cloud and Spot does a depth first search on it. We want to generate states on the fly to improve the performances. For that, we use a kernel probability density estimation. The generated states are then used as starting points for threads which will explore the state space in parallel. +
L'objectif est d'améliorer Spot, une bibliothèque de Model Checking. Spot utilise un type de graphe spécifique dans lequel chaque état est un ensemble de variables avec des valeurs données. Ces valeurs peuvent être vues comme des coordonnées et un état peut donc être vu comme un point à N dimensions. L'espace d'états est alors un nuage à N dimensions et Spot effectue un parcours en profondeur sur celui-ci. Nous voulons générer des états à la volée pour améliorer les performances. Pour cela, nous utilisons une estimation de densité de probabilité par noyau. Les états générés sont ensuite utilisés comme points de départ pour des processus qui exploreront l'espace d'états en parallèle. +
A deterministic automaton can be minimized efficiently into an automaton that has a minimal number of states. The reduction algorithm presented here produces an automaton with a minimal number of states from a non deterministic automaton with weights defined in a field. This algorithm computes the base of the vector space generated by the series represented by the automaton and produces an automaton with a number of states equal to the dimension of this base. To find this base the algorithm has to solve a system of linear equations, this step requires the semiring to be a field. We also want to run our algorithm on fields that are not commutative which forbids the use of classical solvers for these systems. This report shows how we deal with these different constraints. We also present a modified algorithm to work with series over Z semiring which is not a field but has some sufficient properties. +
Vaucanson has been designed to satisfy the needs of the automaticians. There are, however, other fields where automata are widely used. This prospective report will focus on linguistics, and more precisely the automata needs of the natural language processing community since the applications differ from our usual ones. This way, we will be able to assess our range of applicability and usability. First, we will explore the different domains and detail the various needs. Then, we will be able to evaluate whether or not Vaucanson is usable for those domains and, finallydiscuss some potential work leads. +
Attribute grammars are well suited to describe (parts of) the semantics of programming languages: hooked on the syntactic production rules, they allow to express local relations that are later bound globally by a generic evaluator. However they fall short when working on large and complex languages. First attributes that are virtually needed everywhere need to be propagated by every single production rule. Second, this constraint hinders modularity, since adding a syntactic extension might require the propagation of new attributes in the rest of the language. This paper shows how to solve these problems by introducing a technique to automatically propagate attributes by completing the set of semantic rules. We formally define the propagation constraints such that it is optimized to avoid unnecessary addition of semantic rules. Attribute grammars are thus made more maintainable, modular and easier to use. +
Les grammaires attribuées sont plus adaptées pour décrire (des parties de) la sémantique d'un langage de programmation : accrochées sur les règles de production syntaxique, elles permettent d'exprimer des relations locales qui sont par la suite liées entre elles globalement par un évaluateur générique. Cependant elles ne passent pas à l'échelle quand on travaille avec des langages volumineux et complexes. Premièrement les attributs qui sont requis quasiment partout ont besoin d'être véhiculés par chaque règle de production. Deuxièmement, ces contraintes cassent la modularité car le fait d'étendre une grammaire nécessite la propagation des nouveaux attributs à travers le reste du langage. Ce papier montre comment résoudre ces problèmes en introduisant un système de propagation automatique des attributs qui complète l'ensemble des règles sémantiques. Nous avons défini formellement les contraintes de propagations de manière optimisée afin d'éviter l'ajout de règles sémantiques inutiles. Ainsi les grammaires attribuées sont devenus plus maintenables, modulaires et facile à utiliser. +
Atrial fibrillation is a common illness, which can be detected easily if you can localize the human atria in a MRI image. Manual segmentation is labor intensivetherefore here we adapt an automatic method developped for brain image segmentation. Using transfer learning, we retrain a convolutional neural network used for natural image categorization (VGG), and compare the advantages of using a pseudo-3D technique. We also explore ways to preprocess input data to improve final results. +
Our goal is to detect text zones on any type of identity documents from any country and that are recorded by smartphones cameras. Hence, we may segment latin letterscyrillic letters or ideograms. Moreover, some identity papers have watermarks or letters as background pattern that should be filtered. Furthermore, the context of the video (luminosity, background, ldots) has to be taken into account, in order to ensure that the binarized image has a minimal number of components to filter. In this way, the proposed processing, thanks to morphological operatorssegments the text and limits the number of components to process. +
Common Lisp og packages fg provide a functionality similar to og namespaces fg present in C++. They allow to encapsulate symbols that can be either exported or private. The exported ones must be explicitly declared at the package definition. This list is tedious to maintain when developing large projects. In this report will study ways to automatically maintain this list. Several approaches are proposed and compared. +
Our goal is to segment ancient maps of France, being cut and glued on a canvas. The colors in the canvas and in the maps are very close, making the boundary difficult to distinguish. However, pixel-perfect parts of the boundary are obtained thanks to morphological operators. To complete the segmentation, the image is separated, thanks to a maskinto three zones (map, canvas, and a "thick" boundary)which are used by a classification method to obtain results close to the actual boundary. Finally, the first results are corrected thanks to such new knowledge. +
Social media have been extensively used in the attempt to influence users with biased information and rumors. Recently, a new set of accounts know as troll farms have emerged, lauching coordinated disinformation campains. In this regard, we aim to identify the creation of troll farms by studying how they differ from common users and how they attempt to influence them. By leveraging graph analysis techniques we will look into how trolls propagate information through Twitter. Our goal being to build a system capable of recognizing troll farm accounts on trending topics on Twitter. +
VAUCANSON est une plateforme de manipulation d'automates finis et de transducteurs. Après plusieurs années de developpement, il fût constaté que l'interface mise en place pour manipuler les automates était trop complexe. Des travaux furent donc entrepris pour résoudre ce problème, amenant ainsi à l'introduction des "label kinds". Deux versions de la plateforme sont donc en developpement aujourd'hui: VAUCANSON 1.4, qui vise a terminer et compléter le travail effectué avant l'introduction des kinds et VAUCANSON 2.0, dernière version de la plateforme, pour le moment incomplète. Ce rapport a pour but de présenter une nouvelle fonctionnalité de VAUCANSON 1.4, les semi-anneaux Z/nZainsi que le travail en cours sur VAUCANSON 2.0. +
B
Entrainer un réseau de neurones convolutionnel dépends de l'utilisation d'une fonction de coût, qui offre une évaluation de la performance du réseau et permet l'optimisation de celui-ci. Différentes fonctions de coût évaluent la performance de manières différentes, et affectent donc différemment l'entraînement du réseau. Ce rapport a pour but de partager notre progrès dans l'évaluation de la performance de plusieurs fonctions de coût dans l'entrainement de réseaux de neurones convolutionnels pour la segmentation de tumeurs cérébrales. +
Vaucanson is an extensive C++ library for the manipulation of finite state machines. Compared to its main competitorOpenFST, Vaucanson has major performance issues. In order to improve the performance of Vaucanson, a set of tools is required to analyze the library's behavior in terms of CPU time requirements and memory usage. Up to March 2009, no existing tool was fully adapted to Vaucanson and practical to use. CBS is a C++ Benchmarking Suite that measures the performance of C++ projects and provides tools to displayanalyze and compare results in a human-readable form. It is used for in-depth Vaucanson profiling, and it helps the development team rewrite algorithms. +
This report summarizes three methods implemented in the model checking tool Spot. The first method aims at improving the conversion of a program model to a Kripke structure with partial order reduction, a technique where the order of some actions of the program is not considered relevant. This may reduce the size of the Kripke structure. The second method is a modification of the first, which makes it possible to use for LTL properties checking, with any LTL formula. The third method goal is to verify that no livelock may occur in a model, without the need of LTL property. We give benchmarks of all these methods, focusing on testing their common goal: reducing the amount of memory needed, which is an important bottleneck in the model checking field. +
Binary Partition Tree is an efficient structure to store region information for image processing, segmentation and information retrieval. It is a hierarchical structure to simplify operations and recognition on an image. It can use different region models and distance function calculation to create itself. Usually, we construct this tree on a segmented image for efficiency and time saving. All this parameters can variate and change the BPT representation of your image. The resistance of our tree to noise can also be studied, to find out what level of the tree is influenced by the noise. +
Pylene is an image processing (IP) library aiming for high genericity and performance. To accomplish its goals, it was created using C++ templates, allowing for great flexibility and no loss of performance. Pylene is one of the few IP libraries that successfully uses templates, which means it could become a staple in the IP field, but it would first have to overcome a big issue resulting from the usage of C++ templates. That issue is the usability of the library. C++ is not known for its ease of use, and by extension, this makes Pylene hard to use in concrete IP problems. Here, we try to overcome this problem through a Python version of the library. Seeing as though recreating all the library in Python would be nigh impossible, it seems sensible to instead try to bind the high level API to Python. This in itself brings up another issue: the available techniques do not answer our problems well enough, especially in regards to C++ template bindings. Since the idea behind templates of "knowing the type at compile time" doesn't exist in Python, we are faced with a gap between the static world of C++ templates, and the dynamic world of Python. We are presenting in this paper our solution to cross this static-dynamic difference: removing the templates through type-erasure and using contextual information for the type retrieval in Python. +
Spot is a C++ library that relies on the automata theoretic approach to model checking. To represent properties we use LTL-formulae, which are translated into automata. In Spot these automata are Transition-based Generalized Büchi Automata (TGBA). A major issue for a model checker is to be fast. A good way to reach that is to make automata as small as possible. Scientific litterature proposes a lot of algorithm to achieve our goal. Bisimulation and simulation work on '"`UNIQ--math-00000003-QINU`"'-automata. We see in this report how to adapt these algorithms to make them work on TGBA. We will see the profit which is given by the bisimulation implementation. And we deduce the importance to implement the simulation to reduce TGBA. +
L'architecture du projet Vaucanson a été con,cue initialement autour du design pattern Element. Ce dernier a l'énorme avantage de distinguer à la fois les concepts et les implémentations. C'est à dire que pour un type d'automate comme les automates booléens, on peut théoriquement avoir plusieurs implémentations qui se côtoient dans un même programme. Malgré toutes ces précautions, aujourd'hui, ajouter une nouvelle structure s'avère très délicat et remet en cause de nombreux points au sein du projet. C'est pour cette raison que durant ce séminaire nous tenterons de répondre à ces problèmes. Les problèmes de performances qu'a pu rencontrer le projet sont également une bonne motivation pour s'attaquer à ce sujet : il est aujourd'hui indispensable de proposer des nouvelles structures plus efficaces, notamment implémentées avec la bibliothèque Boost. +
Vaucanson est une bibliothèque générique de manipulation d'automates. Le cur de sa généricité réside dans le support de types d'automates variés mais aussi sa capacité à s'appuyer sur différentes structures de données. Actuellementnous avons différentes manières de manipuler des transitions. Cependant, aucune d'entre elles n'est réellement indépendante de la structure de données utilisée. Afin de pallier cela, nous allons nous tourner vers le design pattern Iterator. Nous évaluerons l'impact de ce design pattern sur les performances et sur l'utilisation de la bibliothèque en termes d'écriture d'algorithmes. +
The work performed last year underlined the fact that the overall performance issues of Vaucanson could be widely improved by an internal use of hash tables and, more particularly by the Multi Index from the Boost C++ library. We tried to make good use of the new functionalities provided by Boost. It results in the implementation of a new graph structure. We present in this report the different issues implied by these modifications on the graph implementation and we try to answer to the new issues about the genericity of Vaucanson. +
Suite aux séminaires de l'année dernière, il en ressort que les performances globales de Vaucanson pouvaient largement être améliorées par l'usage de tables de hachage et plus particulièrement les Multi Index de la bibliothèque Boost. Pour ce séminaire, nous chercherons à tirer parti des nouvelles fonctionnalités offertes par Boost. Ceci impliquera l'apparition d'une nouvelle implémentation de graphe. Nous présenterons au cours de ce séminaire les enjeux induits par ces changements sur l'implémentation et tenterons de répondre au problèmatiques soulevées par la généricité de Vaucanson. +
Vaucanson is a generic finite state machine manipulation platform. We have based our genericity on the ability to not only support various types of automata, but also to use different data structures to represent them. In its current state, we have various techniques to iterate over sets of transitions, however, none of them is really independent of the data structures. To overcome this problem, we have integrated the design pattern Iterator. Our goal is to assess the improvements given by this method in terms of performance and code writing. +
L'architecture du projet Vaucanson a été con,cue initialement autour du design pattern Element. Ce dernier a l'énorme avantage de distinguer à la fois les concepts et les implémentations. C'est à dire que pour un type d'automate comme les automates booléens, on peut théoriquement avoir plusieurs implémentations qui se côtoient dans un même programme. Malgré toutes ces précautions, aujourd'hui, ajouter une nouvelle structure s'avère très délicat et remet en cause de nombreux points au sein du projet. C'est pour cette raison que durant ce séminaire nous tenterons de répondre à ces problèmes. Les problèmes de performances qu'a pu rencontrer le projet sont également une bonne motivation pour s'attaquer à ce sujet : il est aujourd'hui indispensable de proposer des nouvelles structures plus efficaces, notamment implémentées avec la bibliothèque Boost. +
Deep neural networks are increasingly used for their capacity to correlate concrete parameters to deduce abstract characteristics. The bottleneck neural network is a specific form of those. This work presents the principle of this kind of network and its use for the reprocessing of Mel Frequency Cepstral Coefficients in a speaker recognition system. Therefore, it is a matter of studying the convergence of such network but also the change in overall system performance. +
The detection of white matter hyperintensities in an efficient way is an important issue in the medical field. Indeed, these hyperintensities are complicated to detect with the naked eye, even for medical personnel. An efficient detection of these hyperintensities would allow a better diagnosis of certain neuro-degenerative diseases but also to avoid certain medical errors. This is the issue we have tried to address in this report. We propose a solution based on a convolutional neural network accompanied by a preprocessing performed on these inputs +
Brain development can be evaluated using brain Magnetic Resonance Imaging (MRI). It is useful in cases of preterm birth to ensure that no brain disease develops during the postnatal period. Such diseases can be visible on T2-weighted MR image as high signal intensity (DEHSI). To assess the presence of white matter hyperintensities, this work implements a new robust, semi-automated frameworkbased on mathematical morphology, specialized on neonate brain segmentation. We will go over the related work, the implementation of the different steps and the difficulties encountered. In the end, the version developped during this internship is not completely finished but it is in good shape for a later finalization. +
Gliomas are a category of brain tumors that have different degrees of malignancy, shapes and textures. Manual segmentation by experts is a challenging task because of the heterogeneity of these tumors. Several methods of automated gliomas segmentation have been studied at MICCAI 2018 BraTS Challenge. We want to improve the segmentation results submitted last year by LRDE's team, using VGG architecture. This convolutional neural networkclassically used for natural image categorization, has been adapted for medical image segmentation through transfert learning and pseudo-3D techniques. Current improvements notably focus on preprocessing, using morphological operators, and will be submitted to this year's challenge. +
With the continuous improvement of quantum technologiesone might wonder if it is possible to take advantage of them for machine learning. In this paper we present a first approach of quantum computing as well as the implementation of a quantum perceptron we then explain the reasoning behind these algorithms. +
Climb is a generic image processing library. Still considered a prototype, Climb already provides tools that simplify the building of image processing chains such as morphers and the operator. In order to extend this aspect of Climb, a GUI has been developed. This GUI allows the construction of processing chains with no knowledge in programming, while providing a visual and interactive feedback to the user. This technical report describes the various components of this interface. Our approach uses the algorithms and tools defined in the library to construct the back-end logic and the interactive aspects of our graphical application. Since genericity is a key feature of Climb, we have been able to extend its scope beyond image processing, and thus show that we are able to use it in different situations such as the construction of a GUI. +
C
Transformers is a C++ manipulation framework built on Stratego/XT. Program Slicing is an important field of program transformation. We will explain what Program Slicing is, give a quick overview of various aspects of Program Slicing and show how Transformers can be turned into a C++ Program Slicing tool. +
C++ is a context-sensitive language that can be parsed using a context-free but ambiguous grammar. Disambiguation is then required to select the unique semantically-valid parse tree. Transformers, a framework for C++ program transformation, uses attribute grammars to achieve that stage. One of the hardest ambiguity in the language is related to metaprogramming. In so far as code is generated when templates are instanciated, types are not fully known at the declaration site. Therefore, type-checking is needed to perfectly handle templates, and it poses a real challenge. This report focuses on template disambiguationdetailing the problems and how to resolve it, in order to provide a better platform for source manipulation. +
Olena is one of the most advanced image processing libraries in terms of genericity. Its fully static design allows for high performance, although sometimes at the cost of overweighted syntax and longer compilation times. This makes it less convenient for incremental developmentexperimentation and rapid prototyping. We will present a different approach to generic image processing which, while using the same domain model as Olena, focuses on dynamicity aspects and offers a totally different use of the library. The cornerstone is the Common Lisp programming language which opens a perspective for interactive use, on-the-fly creation of image types and algorithms as well as a clearcustomizable and extensible syntax for common operations. +
Olena est l'une des bibliothèques de traitement d'images dont la généricité est la plus poussée. Son modèle entièrement statique permet de très bonnes performances, au prix d'une syntaxe alourdie et de temps de compilation importants. Ces aspects la rendent moins efficace pour le développement incrémentall'expérimentation et le prototypage rapide. Nous présenterons une approche différente du traitement d'images générique qui utilise la même modélisation du domaine qu'Olena mais se concentre sur les aspects dynamiques, offrant ainsi une utilisation totalement différente de la bibliothèque. La pierre angulaire est le langage Common Lisp qui permet une utilisation interactive, la création à la volée de nouveaux types d'images ou de nouveaux algorithmes, tout en offrant une syntaxe claire, personnalisable et extensible pour les opérations courantes. +
Ce travail utilise une architecture siamoise pour calculer une similarité. On donne en entrée deux échantillons sur deux sous-réseaux de neurones identiques avec les mêmes poids. Chaque sous-réseau prend en entrée des statistiques sur les données du signal. On peut ensuite calculer la distance entre les informations. Le DNN est capable de projeter les entrées dans un sous-espace de dimension plus basse en apprenant un invariant. On présente les résultats de cette application en s'appuyant sur plusieurs types de statistiques et on les compare aux mesures classiques utilisant PLDA ou la distance cosinus, appliquées à des i-vecteurs. +
Le complexe de Morse-Smale est un outil utile pour analyser la topologie d'une image. Cependant, son calcul est onéreux et il existe plusieurs algorithmes qui poss`dent des différences dans la définition du complexe. D'un autre côté, l'algorithme de coupe de ligne de partage des eaux est un algorithme morphologique qui découpe des images en niveaux de gris. Il interprète les images comme des graphes valués sur les arrêtes, les poids étant donnés par le gradient de l'image. Lidija Comic était la première á mettre en avant une possible équivalence entre l'algorithme de calcul du Morse-Smale et l'algorithme de ligne de partage des eaux, avec des marqueurs spécifiques sur les maxima et les minima de l'image. Dans ce document, nous parlons de cette possibilité et nous proposons une implémentation d'une version modifiée de l'algorithme de coupe de ligne de partage des eaux, qui fonctionne sur un graphe valué sur les sommets pour calculer le complexe de Morse-Smale. +
Calculer le flux optique peut être un premier pas vers l'inpainting vidéo. Pour cette application, nous devons manipuler des séquences avec des zones manquantes, celles à inpainter. Le flux optique peut être calculé de manière locale ou globale. Les méthodes globales ont généralement de meilleurs résultats. Dans le cas de séquences avec des zones manquantes, les méthodes globales ne peuvent pas être utilisées de manière directe à cause du manque d'informations dans ces régions. Dans ce rapport technique, nous présentons une méthode combinant des algorithmes locaux et globaux afin de calculer le flux optique dans ce type de séquences ce qui nous permet d'inpainter efficacement et simplement des vidéos. +
Olena is a generic image processing library developed at LRDE. It provides many morphological algorithms. Mathematical morphology offers several powerful tools in image processing and analysis. Similarities appear when writing morphological algorithms. Thereby, we can classify those tools and then build canvases of algorithms. This report presents what is a canvas and why canvases matter. We will see different manners to implement canvases with their pro and con arguments. Finally, we will explain which canvas implementation we have chosen for Olena and why. +
Olena est une bibliothèque générique de traitement d'images développée au LRDE. Elle propose un grand nombre d'algorithmes morphologiques. La morphologie mathématique, offre des outils très puissants de traitement et d'analyse d'images. Des similarités apparaissant dans l'écriture des algorithmes morphologiques, il est possible de les classifier etainsi, de proposer un certain nombre de "canevas" d'algorithmes. Ce rapport définie ce que sont les canevas et les avantages qu'ils apportent. Apres une brève introduction à la morphologie mathématique, cet exposé presentera différents canevas d'algorithmes retenus par Olena. +
FIXME +
FIXME +
La grammaire du standard du C++ n'ayant pas été conçue pour etre aisément analysable, son utilisation dans le cadre de la manipulation de programme est comparable à la complexité de l'AST généré par celle-ci. Le rôle de Centaur au sein de Transformers est ainsi de fournir une infrastructure générique permettant de manipuler et de synthétiser cet AST : les transformations de programmes sont simplifiées gràce a un accès plus aisé aux informations contenues dans l'arbre syntaxique et ses annotations. Grâce à cette bibliotheque, les tâches répétitives et souvent génératrices d'erreurs, comme l'énumération des éléments d'un conteneur ou la recherche des classes parentes d'une classe, seront factorisées par un ensemble de fonctions correspondant à un modèle modulaire et extensible. +
The C++ standard grammar was not thought to be easily parsable so its use in the context of program handling can be compared to the complexity of the AST generated by it. The aim of Centaur inside Tranformers is to propose a generic framework allowing to manipulate and digest this AST : program transformations are simplified thanks to an easier access to the parse tree data and its annotations. Thanks to this library, repetitive and error-prone tasks like enumerating a container's elements or the parent classes lookup of a class will be factorized by a function set corresponding to an extensible and modular model. +
Climb est une bibliothèque de traitement d'images générique développée en Lisp. Les voisinages sont representés sous la forme d'ensemble de sites (site-set) pour permettre des manipulations génériques sur de multiples types d'images. En parallèle de ce concept, une étude des voisinages pondérés est effectuéeexpliquant différents moyens d'étendre le concept d'une écriture unique des algorithmes pour les exécuter sur différents types de paramètres. Trois implémentations sont proposées, décrites et comparées au niveau de leur généricité et de leur expressivité. +
Climb is a generic image processing library developed in Lisp. Neighborhoods are represented as site-set to allow generic manipulation over multiple pictures type. Along these concepts, a study of weighted neighborhood representation is done, showing how we can extend the concept of writing algorithms once and running them over different parameters type. Three implementations are proposed, described and compared on both genericity and expressivity. +
La programmation orientée contexte est un paradigme prometteur pour prendre en compte les problématiques transverses dans le logiciel. Ce paradigme permet de spécialiser les classes et les méthodes en fonction du contexte. Cependant, il ne traite pas la coercitionc'est-à-dire la conversion d'un objet existant dans un certain contexte vers une nouvelle représentation dans un autre contexte. Nous montrons en quoi ce manque est critique, en fournissant des exemples extraits de Climbune bibliothèque de traitement d'images écrite en Common Lisp. Nous proposons des solutions pour la coercition automatique d'objets, et nous les analysons en termes de simplicité et de généricité. +
The Olena project provides a generic library for image processing, Milena. We want this library to feature many value types so that the user can always choose the relevant types for his application. For instance, we provide many grey-level types, many color types, etc. This seminar focuses on how we implement color types in Milena. There are different color spaces (RGB, HSI, and so on) and several possible encodings for the same color space (rgb_3x8, rgb_f, etc.). One objective of ours is to make things easy for the user. In particular, we want the user to handle color values without being concerned of internal mechanisms. For instance, in conversion formulas, we do not want to see the details of implementation (division by 255). +
go2pins est un outil utilisé pour interfacer un programme Go avec des outils de vérification formelle. À l'aide d'une série de transformations, un programme Go est compilé vers un programme au comportement identique, mais exposant une interface permettant d'itérer dans l'espace d'états de celui ci. Cependantgo2pins ne gère actuellement pas les programmes utilisant des goroutines, qui permettent l'exécution parallèle de fonctions. Dans ce rapport, nous présentons les solutions envisagées pour implémenter ce comportement dans go2pins, ainsi que les problèmes rencontrés. +
Comparaison entre le Fictitious Play et le Fictitious Play Alterné dans le cadre des jeux à somme nulle +
L'algorithme du Fictitious Play est un procédé d'apprentissage itéré utilisé dans le cadre de la recherche des équilibres de Nash. Son principe est simple : à chaque itération, chacun des joueurs “renforce” celle de ses stratégies pures qui est la plus efficace face à ses adversaires. Pour certains jeux, cet algorithme converge vers un équilibre de Nashfournissant ainsi un algorithme d'approximation efficace. La convergence ne peut toutefois être prouvée que pour un nombre limité de cas. L'algorithme du emphFictitious Play Alterné (présenté l'année dernière) en est une variante dans lequel seul le joueur le plus “éloigné” de son gain optimal renforce sa stratégie la plus efficace. Cette étude se focalisera sur une comparaison de l'efficacité de ces deux algorithmes dans le cadre des jeux à somme nulle et abordera également les notions de classification des jeux nécessaires à la réalisation de cet objectif. +
A l'heure actuelle, l'espace des i-vecteurs est devenu l'état de l'art pour les systèmes de reconnaissance du locuteur. La distance cosinus (CD) est la méthode de décision la plus utilisée. Elle utilise l'analyse discriminante linéaire (LDA) et la Within-Class Covariance Normalization (WCCN) afin de compenser globalement le canal. Le but de ce travail est de compenser localement le canal avant d'appliquer la CD. L'idée est de créer un graphe des i-vecteurs partitionné à l'aide d'algorithmes de détection de communautés, puis de projeter les segments test et target dans ce dernier. On sélectionne uniquement leur voisinage pour entrainer la LDA et la WCCN. Les résultats seront comparés avec la méthode de compensation globale. +
Model checking is a field of formal verification which aims to automatically test the behavior of a system with the help of logic formulae. Spot is a model checking library which relies on one technique: the automata-theoretic approach. In this approach, both system and formula are expressed with Büchi automata, which are automata on infinite words. Spot provides several algorithms to deal with these automata, with model checking as objective. However, an algorithm is missing: the complementation of Büchi automata. Because of its high complexity this algorithm is rarely used in practical, but it does not lack theoretical interests. We will present an implementation of this algorithm in Spot. +
Model checking is a field of formal verification which aims to automatically test the behavior of a system with the help of temporal logic formulae. Spot is a model checking library which relies on one technique: the automata-theoretic approach. In this approach, both system and formula are expressed with Büchi automata, which are automata on infinite words. Spot provides several algorithms to deal with these automata, with model checking as objective. An operation for automata was recently added in Spot : the complementation. Research of algorithms for this operation is still relevant today, since there is still no algorithm reaching the theoretical optimal bound. We will present two recent complementation algorithms implemented in Spot. +
Climb is a generic image processing library designed to be used for rapid prototyping. The implementation of two component trees algorithms impacts Climb in several ways: the definition of values is extended, new site sets are added and debugging utilities are improved. A detour is taken to understand the Chaining design pattern popularized by the Javascript jQuery library. The pattern is adapted to both the image processing domain and Common Lisp and is extended to introduce a parallel notation as well as better control flows. +
Pattern recognition and object detection are very important stakes in image processing. Many solutions have been provided; nevertheless the one based on component trees seems to be the most promising. A component tree allows to work on connected components at different gray-levels in the image. Thanks to this tree, we can use attributes as criteria to identify components, such a component being an object in the image. During this seminar, we present a component tree implementation, how to deal with attributes, different methods dedicated to component identification and a general processing chain that leads to object recognition. +
Les transducteurs sont utilisés dans beaucoup de contextes, comme la reconnaissance de parole ou le calcul de la similitude entre protéines. Un des algorithmes fondamentaux pour les manipuler est la composition. Ce travail présente l'algorithme basique de compositionpuis son extension à des transducteurs à transitions spontanées. Une adaptation paresseuse de l'algorithme est ensuite proposée, à la fois pour la composition et pour le pré-traitement (insplitting). Nous montrons ensuite que la version naïve de la composition variadique ne réduit pas la quantité de calculs nécessaires. Enfindes mesures de performances comparent l'implémentation de la composition dans Vcsn à celle d'OpenFST. +
Les transducteurs sont utilisés dans beaucoup de domaines, comme par exemple en linguistique pour modéliser des règles phonologiques, pour les expressions régulières, pour des languages de spécification, pour de la reconnaissance vocale... Quand on les manipule, un outil pour le moins indispensable est la composition. En tant que tel, il est essentiel de l'implémenter dans Vaucanson 2, de manière efficace. Ce rapport va présenter les fondations sur lesquelles s'appuie la composition de transducteurs, puis son implémentation et son optimisation. La composition est considérée ici comme un cas particulier du produit d'automates à transitions spontanées, donc trois algorithmes de produit sont présentés ici, suivi de concepts d'implémentation essentiels. +
Pour représenter un système par un automate, il faut sauvegarder toutes les valeurs des variables du système pour chaque état de l'automate. Cela peut prendre beaucoup de place en mémoire lorsqu'il y a beaucoup de variables et/ou d'états, et de fait ralentit le temps d'exécution à cause des défauts de cache. Pour contourner ce problème dans Spot, on utilise une simple compression du tableau contenant les variables d'un étatet ce pour chaque état, ce qui réduit la mémoire utilisée et aussi le temps d'exécution. Dans ce rapport, nous présentons une structure de données qui améliore la compression des variables en utilisant la redondance des valeurs présentes dans différents états, et les différents problèmes rencontrés lors de son ajout dans Spot. +
Computing optical flow can be a first step towards video inpainting. In such cases, one has to deal with video sequences where some parts, the ones to be inpainted, are missing. On the other hand, the optical flow can be computed either locally or globally. Global methods generally show better results. In the case of sequences with missing areas, the computation with global methods is not straightforward due to the lack of information in some regions. In this technical report, we introduce a method combining both global and local algorithms in order to compute the optical flow in such sequences, leading to an efficient and simple way to compute video inpainting. +
At the end of this decade will arise C++0x and with it the new “concept” paradigm. Concepts provide abstract types as well as all the equipment to adapt concrete types to their abstraction, just like Static library, a part of Olena project, does. We compare these two approacheshighlighting their respective strengths and weaknesses, in order to lay the foundations for the integration of concepts into SCOOP. In fact, concepts will simplify the client code and bring some new features to SCOOP. +
Climb est une bibliothèque de traitement d'images générique. Elle est implémentée en Common Lisp et vise un dynamisme et une facilité d'utilisation maximaux. Dans ce but, l'interface utilisateur doit être à la fois suffisamment puissante pour ne pas cacher certaines fonctionnalités de la bibliothèque sous-jacente, et intuitive pour l'utilisateur. La difficulté est de créer une interface faisant un minimum de compromis entre ces caractéristiques, tout en restant suffisamment extensible pour les garder quand la bibliothèque évolue. Après quelques rappels sur le design générique de Climb, nous présentons les modifications que nous avons apportées à l'interface existante pour améliorer son utilisabilité sans restreindre ses capacités. +
Climb est une bibliothèque de traitement d'image générique. Encore à l'état de prototype, Climb fournit déjà un certain nombre d'outils comme les morphers et l'opérateur qui permettent de simplifier la définition de chaînes d'algorithmes. Afin de prolonger cet aspect, une interface graphique a été développée. Celle-ci permet de construire des chaînes de traitement d'image sans connaissance en programmationtout en offrant un retour à la fois visuel et interactif. Notre approche utilise les algorithmes et outils définis dans la bibliothèque pour construire la logique interne de l'application ainsi que ses différents aspects interactifs. La généricité étant l'une des caractéristiques principales de Climb, nous avons été capables d'étendre son champ d'application au-delà du traitement d'image et ainsi montrer qu'elle peut être utilisée dans des situations différentes telles que la construction d'une interface graphique. +
Les technologies quantiques étant en évolution constante, il est normal de se demander s'il est possible de prendre avantage de ces technologies dans le domaine de l'intelligence artificielle. Dans ce papier, nous présentons les rudimentaires de l'informatique quantique ainsi que l'implémentation d'un perceptron avec comme support une machine quantique et une explication de son fonctionnement. +
Context-oriented programming is a paradigm that addresses crosscutting concerns and context-dependent behavior in a program. This paradigm makes it possible to express aspects of a program behavior that are orthogonal to the object model, while maintaining its abstraction and modularity. In the domain of image processing, for instancecontext-oriented programming may be used to model aspects related to the structure of an image, its content or even its memory representation. We present context-oriented programming, and we analyze the crosscutting concerns existing in Climb, an image processing library written in Common Lisp. We then explain how context-oriented programming solves those concerns. Finally, we analyze the advantages of context-oriented programming in the domain of image processing +
C++ provides a good support for performance and genericity through templates. However, it has a real cost on flexibility and compilation time. In order to overcome these issues, Vcsn introduces a dynamically-typed library named dyn. The purpose is to bring more flexibility to the project and it also allows just-in-time compilation. This work presents, first of all, our thoughts on how to handle and optimize our compile time, then various improvements added to dyn. +
Le C++ fournit un bon support pour la performance et la généricité notament grâce aux templates. Cependantcela a un réel coût au niveau dela flexibilité et du temps de compilation lorsqu'un programme devient assez conséquent. Pour palier cela Vcsn introduit une couche nommée dyn:: ayant pour but d'apporter de la flexibilité et permettant entre autre un système de compilation à la volée. Ce travail présente nos réflexions sur comment gérer et optimiser nos temps de compilation ainsi que des améliorations apportées à la couchedyn::. +
Spot is an '"`UNIQ--math-00000006-QINU`"'-automata manipulation library who aims to help doing '"`UNIQ--math-00000007-QINU`"'-automata-theoretic approach to model checking or develop tools for '"`UNIQ--math-00000008-QINU`"'-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each '"`UNIQ--math-00000009-QINU`"'-automaton. Of those algorithms, emptiness check algorithms and counterexample search algorithms are often used, with various goals, and since their results are linked, they are often used together. However, some implementations of emptiness check algorithms lack a similar counterexample search implementation which is able to work in the same way on the same automata. We introduce two implementations of counterexample computation, which complete two already existing implementations of emptiness check algorithms by walking in their footsteps and reusing some of the data they gathered to efficiently compute counterexamples. +
In order theory, an antichain is a subset of elements incomparable with one another, following a given order. In the automata theory, some algorithms use antichains as data structures to store sets of states all disjointed, in simulation algorithms to reduce an automaton for example. The implementation of antichain consists to verify at the insertion if the new element is not comparable to another already in the antichain, which is costly because at each insertion we need to do a linear path. In this report, we detail different algorithms to implement the antichain optimizing the insertion of a new element. Then we will show the results of these implementations with our model checker Spot to compare their performances. +
Création d'un lien entre une bibliothèque de traitement d'image en C++ hautes performances vers Python +
Pylene est une bibliothèque de traitement d'image codée pour un maximum de performances et de généricité grâce à des templates. Malheureusement, les templates rendent le code difficile à comprendre et à utiliser facilement. Pour cette raison, nous présentons ici une manière de résoudre ce problème au travers d'une transition de la bibliothèque vers Python. Réécrire toute la bibliothèque en Python serait long et inefficace. Il a donc été préféré d'utiliser des techniques pour exposer Pylene en Python. Le probléme devient donc le suivant: puisque le concept des templates de "connaître le type à la compilation" n'existe pas en Python, nous présentons ici notre solution afin de faire disparaître les templates grâce à de l'effacement de type et de l'information contextuelle. +
Dans la théorie des ordres, une antichaîne est un sous-ensemble d'éléments tous deux à deux incomparables selon un ordre donné. Dans la théorie des automates, certains algorithmes utilisent les antichaînes comme structures de données afin de stocker des ensembles d'états d'un automate tous disjoints. Par exemple elles sont utilisées dans des algorithmes de simulation utilisés pour la simplification de l'automate. L'implémentation d'une antichaîne consiste à toujours vérifier que les éléments insérés dans l'antichaîne ne sont pas comparables à un déjà présent, ce qui rend coûteux l'opération d'insertion car il faut faire à chaque fois un parcours linéaire des données. Dans ce rapport, nous proposons différents algorithmes pour implémenter l'antichaîne en optimisant l'insertion d'un élément. Nous présenterons ensuite les résultats de ces implémentations avec le model checker Spot pour pouvoir comparer leurs performances. +
D
Vcsn est une plateforme dédiée à la création et la manipulation d'automates et transducteurs finis, avec ou sans multiplicités. Elle est composée d'une couche C++ rapide et performante ainsi que d'une interface web Python 3 (Jupyter) plus simple d'utilisation. L'objectif de ce travail est d'ajouter de nouvelles fonctionnalités intuitives et pédagogiques à la couche Jupyter. L'utilisateur doit facilement accéder à tous les outils (génération d'automates et utilisation d'algorithmes sur eux) que propose la plateforme à ce jour. +
There is a hierarchy of temporal properties, defined by Manna and Pnueli (1990). This hierarchy contains, amongst others, the recurrence and persistence classes. Knowing that a formula of linear time temporal logic (LTL) '"`UNIQ--math-0000003F-QINU`"' is recurrent (respectively persistent) is interesting because it ensures that '"`UNIQ--math-00000040-QINU`"' can be translated into a deterministic Büchi automaton (respectively into a co-Büchi automaton). Originally, Spot, a library for '"`UNIQ--math-00000041-QINU`"'-automata manipulation, had a single way to decide if a linear temporal logic formula belongs to the recurrence or to the persistence class. Thanks to our previous work introduced in emphA co-Büching Toolbox +
SCRIBO, for Semi-automatic and Collaborative Retrieval of Information Based on Ontologies, is a document image analysis and semi-automatic analysis project aiming to establish algorithms and collaborative tools in order to extract knowledge from texts and images. The extraction of the different structures of a digitalized document is based on the setup of a processing chain composed of crucial steps to optimize the quality of the rendering. The deskewing of images, prior to the processing chain, is a necessary step that corrects a possible angle due to the digitization of the document. Moreover, the extraction and the study of the characters composing the text, like the average color, the average boldness or the skeleton, not only enables a reconstitution of the text as accurate as possible, but also prepares this one for the OCR. Therebywe will first introduce an algorithm providing a quick detection of the skew angle of a document for little angles, and then the study conducted to extrct different character features. +
Climb is a generic image processing library. It is implemented in Common Lisp and aims at maximal dynamism and ease of use. To achieve such a goal, the user interface must be at the same time powerful enough to avoid hiding some functionality of the underlying design, and intuitive for the user. The difficulty is to design an interface which makes as few trade-offs as possible between these characteristics, while staying extensible in order to keep them as the library grows. After a few reminders about the generic design of Climb, we present the modifications we made to its existing front-end to improve its usability without restraining its capabilities. +
Botnets are one of the most common and powerful cyber attacks tools, from DDoS attacks to crypto currencies mining. Due to the extreme diversity of Botnets types and interactions, it is very difficult to detect their influence using pay-load data only. Within this contextthe goal is to build a Botnets detection system using metadata information from network flows. To do so, we propose a new system based on probabilistic machine learning techniques using Hidden Markov Models to model interactions inside of suspicious networks. Our work is based on a dataset from the Stratosphere project released in 2014. +
The generation of different videos is important for the training of an artificial intelligence. Finding a way to generate realistic marine images by computer helps ensure this generation. In more details, we want to generate videos and metadata associated with the video. Metadata helps us to check and correct our artificial intelligence. To generate those videos, we use use the software MAYA. This software allows us to generate marine environment and extract some images and videos. MoreoverMAYA supports Python's scripts. With Python, we can automate the generation of videos. +
The goal of this project is to increase security during boat's navigation. Using an artificial intelligence which analyses images allows to identify different kinds of danger that a boat can encounter during its navigation. Artificial intelligence can detect a man at sea and alert the boat's crew to help him. To develop this artificial intelligence, a dataset of different marine videos is needed to assure the maximum of situations in the marine environment. Generate a lot of realistic videos by computer is mandatory to train this artificial intelligence. +
Spot is a C++ library that relies on the automata theoretic approach to model checking. To represent properties we use LTL-formulae, which are translated into automata. In Spot these automata are Transition-based Generalized Büchi Automata (TGBA). A major issue for a model checker is to be fast and to consume the memory as less as possible. A good way to reach that is to make automata as small as possible. Scientific litterature proposes a lot of algorithm to achieve this goal. Simulation works on automata which recognizes words of infinite length thanks to acceptance states. We see in this work how to adapt this algorithm to make it works on TGBA. We will see the profit which is given by the simulation implementation on Spot. +
La séparation lettre/non-lettre est un sujet important dans le domaine de la reconnaissance optique de caractères. Il s'agit de déterminer si une surface délimitée d'une image est une lettre ou non, avec une invariance en rotation. Afin de générer un modèle basé sur les données d'entraînement, on analyse les composantes principales (PCA), puis on applique un algorithme d'analyse linéaire déterministe et probabiliste (PLDA). Le modèle ainsi générer sera comparé à celui actuellement utilisé dans l'application de reconnaissance optique de caractères d'Olena. +
Climb est une bibliothèque de traitement d'images générique. L'interface générique d'un algorithme nécessite souvent plusieurs implémentations différentes spécialisées. Olena, une bibliothèque C++, a résolu ce problème en rajoutant des propriétés. Nous allons présenter un moyen de rediriger un appel de fonction vers la meilleure implémentation spécialisée grâce aux propriétés dans un langage de programmation dynamique: Common Lisp. Nous allons ensuite montrer des exemples d'algorithmes et de propriétés utilisées dans le domaine du traitement d'images. +
A distance transform, also known as distance map or distance field, is a representation of a distance function to an object, as an image. Such maps are used in several applications, especially in document image analysis. Some optimizations can be obtained by less generic methods: for example, maps calculated by front propagation can determine shorter paths, assuming that the image is non-convex. This presentation discusses different distance transform algorithms and underlines their advantages and weaknesses. Finally we will explain our choices. +
Une carte de distances est une représentation sous forme d'image d'une fonction distance à un objet. Ces cartes sont utilisées dans de nombreuses applications, en particulier en analyse d'images de documents qui nous serviront d'illustration. Certaines méthodes de calcul de cartes moins génériques que d'autres peuvent s'avérer plus rapides : par exemple, des cartes calculées par propagation de fronts permettent de déterminer des plus courts chemins mais ne fonctionnent que lorsque le support est connu pour être non-convexe. Cette présentation fait un tour d'horizon des différents algorithmes de calculs de cartes de distances, met en évidence leurs atouts et faiblesses et explique les choix retenus. +
In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data structures, we can use parallel or distributed algorithms. In this report, we present an implemention of a distributed state space exploration algorithm proposed by Camille Coti in "One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters". We compare it against a synchronous algorithm and an asynchronous algorithm using threads to communicate with the same machine. We give benchmarks of all these algorithms using the BEEN benchmark. +
The extraction of the different structures of a digitalized document is based on the setup of a processing chain composed of crucial steps to optimize the quality of the rendering. The document layout analysis, meaning the extraction of lines structures, paragraphs, constitutes the core of the processing because the rendering is closely correlated with the text used to fed the OCR system. Thereby, we will introduce a hybrid document layout analysis approach developed under the SCRIBO project. +
The impact of domain mismatch when the system training data and the evaluation data are collected from different sources remains a challenge. This study lays out state-of-the-art techniques used for domain mismatch compensation such as a library of whitening transforms and the use of a dataset-invariant covariance normalization matrix to obtain domain-invariant representations of feature vectors. +
Bien que le développement des systèmes d'analyse discriminante linéaire probabiliste (PLDA) basés sur les i-vecteurs a donné lieu à des résultats prometteurs en reconnaissance du locuteur, l'impact du domain mismatch lorsque les données d'entraînement du système et les données d'évaluation proviennent de sources différentes reste un défi. Le workshop de reconnaissance du locuteur de 2013 de l'Université Johns Hopkins (JHU), pour lequel un corpus d'adaptation du domaine (DAC13) a été crééa travaillé à trouver des solutions pour résoudre ce problème. Ce rapport de recherche présente les techniques de pointe utilisées pour la compensation du domain mismatch ; comme une combinaison de plusieurs transformées de blanchiment, et la normalisation de la covariance indépendante du jeu de données pour obtenir des représentations des données d'entraînement de la PLDA invariantes par rapport au domaine. Ces techniques sont évaluées sur le corpus DAC13 et comparées. +
FIXME +
FIXME +
Static C++ allows designers to develop efficient and generic libraries, but for the end user such libraries are very restricting. Indeed compilation cycles are so long that it forbids prototyping. To overcome this shortcomingwrappers generators such as SWIG allow to pre-instantiate static classes and functions and then make them available in a higher-level language. In our opinion, such approaches have drawbacks. They force the end user to learn a new language to use a C++ library and they can not use classes or functions if they are not available yet. From users feedback, what is really needed is a way to use static C++ from within a C++ dynamic environment and without facing deadly compilation times. To respond to that need, we developed a C++ environment that allows static C++ functions and classes manipulation. We use just in time compilation with a cache system to compile classes and functions on demand. Using advanced C++ programming techniques, we manage to rend the usage of our environment very handy for the end user, thus allowing fast and efficient prototyping. +
Static C++ allows designers to develop efficient and generic libraries, but for the end user such libraries are very restricting. Indeed compilation cycles are so long that it forbids prototyping. To overcome this shortcomingwrappers generators such as SWIG allow to pre-instantiate static classes and functions and then make them available in a higher-level language. In our opinion, such approaches have drawbacks. They force the end user to learn a new language to use a C++ library and they can not use classes or functions if they are not available yet. From users feedback, what is really needed is a way to use static C++ from within a C++ dynamic environment and without facing deadly compilation times. To respond to that need, we developed a C++ environment that allows static C++ functions and classes manipulation. We use just in time compilation with a cache system to compile classes and functions on demand. Using advanced C++ programming techniques, we manage to rend the usage of our environment very handy for the end user, thus allowing fast and efficient prototyping. +
Les tests de vacuité permettent de savoir si le langage reconnu par un automate et vide ou non. Ces tests sont souvent utilisés dans le model checking : malheureusement, ils sont très coûteuxparticulièrement sur les automates qui ne sont ni faibles ni terminaux. Dans le but de réduire ce test coûteuxce travail implémente une option permettant d'extraire trois automates plus petits regroupant les composantes terminales, faibles et fortes de l'automate original, de facc on à ce que trois tests de vacuité correspondants puissent être effectués indépendamment en utilisant l'algorithme le plus approprié. +
On cherche à segmenter d'anciennes cartes de France qui ont été découpées en morceaux puis recollées sur du tissu. La frontière exacte entre carte et tissu est difficile à distinguer car leurs couleurs sont très similaires. Grâce à des filtres morphologiques, on obtient des parties de la frontière au pixel près. Pour finaliser la segmentation, on définit un masque séparant l'image en trois zones: carte, tissu et "frontière épaisse" qui, à l'aide d'une méthode de classification, permet d'obtenir des résultats proches de la frontière réelle. Cette nouvelle connaissance est alors utilisée pour corriger les premiers résultats. +
Transformers est un emsemble d'outils basés sur Stratego/XT permettant la manipulation de programmes C++. Le découpage de programmes est un domaine important de la transformation de programmes. Nous allons expliquer ce qu'est le découpage de programmes, donner un aperc cu rapide de ses différents aspects et montrer comment Transformers pourrait être utilisé comme un outil permettant le découpage de programmes. +
Lorsque l'on essaye d'extraire du texte en inverse vidéo (couleur claire sur fond foncé), nous verrons lors de la présentation de Coddy Levi que de nombreux problèmes surgissent. Le plus courant d'entre eux est la superposition entre ce texte en inverse vidéo, et celui en couleur foncée sur clair. Nous montrerons donc dans cette présentation comment faire un choix entre ces lignes en superposition, en considérant différents critères et en les pondérant. +
Malgré sa sensibilité au contexte, le C++ est analysable avec une grammaire hors-contexte mais ambigüe. La désambiguïsation est ensuite nécéssaire pour sélectionner le seul arbre syntaxique sémantiquement valide. Transformers est une collection d'outils pour la transformation de programmes C++ qui utilise les grammaires attribuées pour réaliser cette étape. Une des plus difficiles ambiguités dans le langage concerne la méta-programmation. Puisque du code est généré à l'instanciation, tous les types ne sont pas nécéssairement connus à la déclaration. La vérification des types est donc obligatoire pour traiter totalement le cas des patrons, ce qui pose un véritable défi. Ce rapport se concentre sur la désambiguïsation des patrons de type et détaille les problèmes et leur méthode de résolution, afin de fournir une meilleure plateforme de manipulation de sources. +
Les réseaux sociaux sont devenus intensément utilisés dans le but d'influencer la population avec des informations fausses ou fortement biaisées. Récemmentnous avons vu naître l'apparition de nouveaux types de comptes lan,cant des campagnes de désinformation. Nous cherchons à identifier ces comptes connus sous le nom de troll farm en étudiant comment ils se différencient des autres utilisateurs et la maniére dont ils cherchent à les influencer. En se servant d'outils d'analyses de graphe, notre objectif est d'identifier l'empreinte sous laquelle ils vont diffuser l'information au sein de Twitter. Le but final étant d'établir un système capable de reconnaître les trolls sur des sujets d'actualités. +
On cherche à détecter les zones de textes sur tout type de pièces d'identité, pouvant provenir de n'importe quel pays et filmées par des caméras de smartphones. Par conséquent, on peut être amené à segmenter des lettres latines, cyrilliques ou des idéogrammes. Par ailleurs, certains papiers d'identité possèdent des filigranes et/ou un fond utilisant des lettres comme motif, qui doivent être filtrés. De plusle contexte de la prise de vue (luminosité, fond...) doit être pris en compte afin, qu'une fois l'image binarisée, le nombre de composantes à filtrer soit minimal. Ainsi, le pré-traitement proposé permet, à l'aide de filtres morphologiques, de détecter le texte efficacement en limitant le nombre de composantes à traiter. +
Le but de ce projet est de pouvoir améliorer la sécurité lors de la navigation de bateaux. L'utilisation d'une intelligence artificielle analysant des images provenant de caméras implantés sur le mât permettra d'identifier les différents dangers auquel qu'un bateau peut rencontrer en milieu marin. L'intelligence artificielle pourra détecter un homme à la mer, alerter l'équipage afin qu'il puisse le secourir. Pour développer une intelligence artificielle, il faut un base de données avec différentes vidéos marines pouvant couvrir le maximum de situation rencontrées en milieu marin. Il faut réussir à réaliser un maximum de vidéos marines suffisament réalistes depuis un ordinateur à l'aide de différents outils. +
La génération de différentes vidéos est importante pour l'entrainement d'une intelligence artificielle. Trouver un moyen de générer des images marines réalistes par ordinateur permet d'assurer cette génération. Plus précisément, nous voulons générer des vidéos et des metadonnées associées aux vidéos. Les métadonnées nous permettront de vérifier et corriger notre intelligence artificielle. Nous utilisons le logiciel 3D MAYA pour développer nos vidéos. Ce logiciel permet de générer des environnements marins et de pouvoir en extraire des images. De plus, l'utilisation de scripts Python est possible avec le logiciel MAYA. Cela permet d'automatiser la génération d'images et de vidéos. +
La détection de logotypes et d'invariants dans une image a pour but de trouver parmi une image (ou une séquence d'images) un élément graphique nouveau ou déjà répertorié qui caractérise une marque, entreprisepersonne, etc. De tels éléments peuvent se retrouver dans de nombreuses images naturelles mais également dans des images publicitaires. Le problème de la détection consiste non seulement à effectuer des comparaisons avec des éléments déjà rencontrés mais également à mettre en place un système d'apprentissage permettant de désigner de possibles nouveaux logotypes. L'intérêt de l'intégration d'un tel outil dans la plate-forme de traitement d'images Olena et possiblement au sein du projet Terra Rush permettrait de mieux indexer les contenus mais également d'invalider des zones de l'image dans d'autres chaînes de traitement. Dans ce rapport, nous expliquerons principalement une méthode générique permettant de localiser les points-clés invariants d'une image : les descripteurs SIFT. +
La détection d'éléments discriminants dans une image est un sujet très actif de vision par ordinateur. Aujourd'hui, les applications sont très diverses, allant de la robotique à la photographie numérique assistée. Notre exposé se concentrera sur la détection de logotypes dans des images naturelles. Pour ce faire, nous nous basons sur Olena, une plateforme libre, générique et performante de traitement d'images afin d'implémenter un détecteur de points-clés : les descripteurs SIFT. +
La détection de voix a de nombreuses applications. C'est par exemple une étape obligatoire avant de faire de la reconnaissance du locuteur. Ce rapport présente deux différents types d'algorithmes pour la détection de voix (VAD) : un utilisant des seuils et le second utilisant des mélanges de gaussiennes (GMM).Les algorithmes proposés utilisent des caractéristiques calculées sur des petits intervalles de temps comme par exemple l'énergie, la monotonie spectrale ou les Mel-Frequency Cepstral Coefficients (MFCC). Les différents algorithmes de détection de voix sont comparés dans différentes conditions de bruit afin de mettre en évidence leur robustesse aux bruits. +
Détection des comportements de botnets au travers d'un flux en réseau en utilisant des modèles de Markov cachés +
Les attaques par Botnets se sont répandues comme l'une des plus grandes cybers menaces, des attaques DDoS au minage de crypto monnaies. La vaste diversité des profils et utilisations des Botnets en font des entités difficiles à détecter en analysant uniquement le contenu des paquets reccus sur une machine. Dans ce contexte, l'objectif est de construire un système de détection des Botnets à partir des méta informations fournies par les flux réseaux. Pour cela, nous proposons un nouveau système basé sur des techniques d'apprentissage automatique probabilisite utilisant les Modèles de Markov Cachés pour modéliser les interactions au sein de réseaux suspicieux. Nos travaux sont réalisés depuis un jeu de données provenant du projet Stratosphere publié en 2014. +
E
Climb est une bibliothèque générique de traitement d'images en Lisp. L'étude de l'implémentation d'un algorithme de segmentation par ligne de partage des eaux permet de faire état des possibilités offertes par un langage dynamique tel que Lisp allié á une modélisation générique des images. Cette étude de cas permet d'aborder les concepts de base de la manipulation d'images au sein de Climb tels que les sitesles ensembles de sites et les accumulateurs. L'utilisation de l'ensemble de ces notions reposent sur l'aspect dynamique et fonctionnel de Lisp. +
Efficiency comparison between Fictitious Play and Alternate Fictitious Play algorithms on the restricted set of zero-sum games +
The Fictitious Play algorithm is an iterate learning process created to compute Nash equilibria. At each iteration of this algorithm, each of the players “strengthens” the strategy that has the highest utility in the current context. For some specific game classes this algorithm converges to a Nash equilibrium, therefore providing an efficient approximation method. Howeverconvergence can only be proved for a small amount of game classes. The Alternate Fictitious Play algorithm (introduced last year) is a variant in which only one player at a time strengthens one of his strategies : the player which is the “further” from his maximum payoff. This study will focus on a comparison of these two approaches on the restricted set of zero-sum games. It will also present the notions of game classification used for this comparison. +
Transducers are used in many contexts, such as speech recognition or in order to measure the similarity between proteins. One of the core algorithms to manipulate them is the composition. This work presents the basic composition algorithm, then its extension to transducers with spontaneous transitions. A lazy adaptation of the algorithm is then proposed for both the composition and the necessary pre-processing (insplitting). Naïve variadic composition is shown to be useless in reducing the amount of computations. Finally, some benchmarks show how the implementation of the composition in Vcsn compares with OpenFST. +
In the automata-theoretic approach to Linear Temporal Logic (LTL) model checking, the negation of an LTL formula is translated into an '"`UNIQ--math-00000003-QINU`"'-automaton. The construction of a smaller automaton reduces a lot the runtime and the memory consumption of the subsequent operations in the model checking pipeline. Müller and Sickert presented an efficient method to translate any LTL formula into a small deterministic automaton. This method consists in splitting the formula into three sets of subformulae which are respectively taken from the (co-)safety fragment, the fairness fragment and the rest. Then they translate all sets of subformulae apart from each other into deterministic automata and they combine these resulting automata. Spot can already translate obligation formulae into minimal deterministic automata. Since obligation formulae are a superset of (co-)safety formulae, we replace the (co-)safety fragment by the obligation fragment to generalize the translation of Müller and Sickert. Concerning the fairness fragment, they showed an efficient translation algorithm that produces small deterministic automata. They also showed a method to compute an efficient product of these automata with other automata. We present how these two methods are implemented in Spot. +
One of the remaining problems with Nash equilibria is the lack of efficiency of best known algorithms. In general case their worst complexity is '"`UNIQ--math-00000036-QINU`"'. Those algorithms are usually old, and aren't likely to be improved. This study focuses first on main algorithms and methods and explains their advantages and their weaknesses. It then introduces a new algorithm developed at the LRDE based on a geometrical approach: a TOP computing method in '"`UNIQ--math-00000037-QINU`"' dimensions. +
L'un des principaux problèmes rencontrés lors de la recherche d'équilibres de Nash est le manque d'efficacité des principaux algorithmes. La plupart ont des complexités en pire cas de l'ordre de O(4^n) . Il n'est de plus que peu probable de réussir à améliorer ces algorithmes, qui sont pour la plupart relativement vieux. Cette étude détaille tout d'abord les algorithmes principaux en spécifiant leurs avantages et inconvénients, puis présente un nouvel algorithme développé au LRDE basé sur une approche géométrique : le calcul du TOP en dimension d . +
Mathematical morphology has become an indispensable tool for an image processing library. The algorithms produced using this technique are very efficient and allow very satisfactory results, in particular for image segmentation operations. The work produced therefore aims to implement and integrate hierarchical morphological representations into the Pylene library. Our work has mainly focused on the global segmentation pipeline using these methods, as well as visualization using saliency maps. The objective being of course to achieve the most optimized algorithms possible to be able to use them on large images. +
This report exposes some performant and generic ways to implement removal of spontaneous transitions in an '"`UNIQ--math-00000017-QINU`"'-NFA. We compare two different approches: the weighted '"`UNIQ--math-00000018-QINU`"'-closure algorithm of J. Sakarovitch and S. Lombardy, and the '"`UNIQ--math-00000019-QINU`"'-removal algorithm of M. Mohri. We discuss how these algorithm can be implemented when dealing with generic weighted automata, and their implications on performance by comparing some empirical results obtained in Vcsn. +
Estimation de la fonction de niveau de bruit dans des images multivariées en utilisant l'arbre des formes et des statistiques non-paramétriques +
De nos jours, de nombreuses applications du traitement d'image nécessitent de connaitre le niveau de bruit dans une image, soit pour le prendre en compte dans ces traitements, soit pour le supprimer. Pour cela, nous avons développé une méthode qui permet d'estimer ce niveau de bruit, modélisé par la fonction de niveau de bruitpour des images en niveau de gris puis nous l'avons étendu aux images multivariées en utilisant des hypothèses simplifiées. Ce semestre, nous avons introduit de nouveaux outils pour améliorer notre méthode et supprimer les hypothèses définies au précédent semestre. +
Estimation de la fonction de niveau de bruit dans des images naturelles en utilisant l'arbre des formes +
De nos jours, de nombreuses applications ont besoin de connaître le niveau de bruit dans une image. Une méthode a déjà été développée pour connaître la fonction de niveau de bruit dans une image en utilisant la détection de blocs homogènes, et a été étendu à la détection de formes homogènes en utilisant l'arbre des formes. Néanmoins, cette méthode ne fonctionne que pour les images en niveau de gris. Nous essayons donc d'étendre cette estimation aux images couleur, les pixels étant multivariées. +
Estimation of the Noise Level Function in Multivariate Images using the Tree of Shapes and non-parametric statistics +
Nowadays, a lot of image processing applications need to know the noise level of an image to take it into account in these processes or to remove it. To do so, we developed a method to estimate the noise level, modeled by the noise level function, for grayscale images, and then for multivariate images, using simplifying hypotheses. This semester, we introduced new tools to improve this method and to remove the simplifying hypotheses defined the last semester. +
Nowadays, a lot of applications need to know the noise level in an image. A method had already been developped to know the noise level function in an image using the detection of homogeneous blocks and has been extended to the detection of homogeneous shapes, using the tree of shapes, which fits better the image content. However, this method is limited to grayscale images. So we aim to extend this estimation to color images, the pixels being multivariate. +
L'objectif principal de la reconnaissance des formes est de permettre aux ordinateurs de reconnaître des éléments sans nécessiter une quelconque intervention extérieure. Cependant, un problème récurrent provient des transformations telles la translation ou la rotation qui peuvent être appliquées à l'image d'origine. Ainsi, différents moments calculés sur l'image ont suscité un intérêt particulier du fait de leur invariance à plusieurs des transformations rencontrées. Un certain nombre d'algorithmes basés sur les invariants de forme sont populaires en analyse d'image de documents et en particulier en ce qui concerne les systèmes de reconnaissance optique de caractères puisqu'ils offrent une caractérisation pertinente permettant la différenciation des lettres. Ils trouvent également un intérêt dans l'analyse de la mise en page de documents en fournissant des informations qui peuvent être utilisées pour différencier les éléments textuels des éléments non textuels. Ainsi, nous présenterons le concept de moments ainsi que l'évaluation de six invariants de forme issus de l'état de l'art dans le cadre de la classification texte / non-texte. Un algorithme d'invariants de forme inspiré du principe du compressive sensing est également proposé. +
La fin de cette décennie verra l'avènement de C++0x et avec lui du nouveau paradigme de og concepts . Les concepts fournissent un mécanisme de typage abstrait pour les types paramétrés ainsi que tout l'équipement d'adaptation des types concrets à ces types abstraits comme le fait actuellement la bibliothèque emphStatic +
Several methods to evaluate text detection algorithms exist. However, they give different results, so it is difficult to estimate their relevance. In order to evaluate these methods, the proposed solution is to compare the automatic evaluations with the human evaluation by considering the latter as a reference. In order to obtain this reference, a website has been created so that a large number of users can easily classify the results of a large number of text detection algorithms on large image bases. The user interface has been developed to minimize the number of comparisons that the user must make in order to obtain a consistent ranking. The website will be tested with the results of the 2013 ICDAR competition, which is composed of height methods on a data set of 233 images. +
Dans le domaine du "model checking", les structures de données utilisées pour représenter un programme ne peuvent être stockées en mémoire à cause l'explosion combinatoire. Pour accélérer l'exploration de structures de données aussi grandes, nous pouvons utiliser des algorithmes parallèles ou distribuès. Dans ce rapport, nous présenterons une implemention d'un algorithme d'exploration d'espace d'état distribuè proposè par Camille. Nous le comparerons avec un algorithme synchrone et un algorithme asynchrone utilisant des threads pour communiquer sur la même machine." +
go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. However, go2pins currently doesn't support programs that use goroutines, Go's concurrency primitives. In this report, we present the various solutions we've assessed to implement this behaviour inside go2pins, and the problems we've had to solve along the way. +
Le texte sujet à extraction via l'analyse de document peut être présent dans deux formes : foncé sur fond clair ou clair sur fond foncé, appelé Inverse Video. Ce rapport explique les problématiques liées à l'extraction de l'inverse video dans Scribo en utilisant la chaîne de traitement déjà existante, les problèmes ainsi introduits et les pistes explorées pour l'amélioration des résultats. +
Nous allons présenter une méthode permettant de différencier le texte du non-texte dans une image en utilisant des descripteurs inspirés des algorithmes de compression de données. L'objectif principal de cette approche est de calculer un signal qui va permettre à des systèmes d'apprentissage supervisés (comme des kppv ou des machines à vecteurs de support) de classifier le texte et le fond d'une image. Afin de calculer ce signalnous utiliserons des méthodes à base d'ondelettes similaires à celles utilisées dans les formats de compression jpeg ou png. Nous allons également étudier quelles ondellettes produisent les meilleurs résultatsavec quel système d'apprentissage et comparer cela avec d'autres descripteurs, qui ne sont pas à base d'ondelettes. Enfin, nous verrons comment il est possible de diminuer le temps de calcul néscessaire pour ces descripteurs en utilisant l'élévation en ondelette et des méthodes optimisées pour calculer l'image polaire. +
F
Last year, we started to work on a new proposal of an XML automata description format, now called FSMXML. This year we are presenting a final version of our work. It takes the form of an rfc. FSMXML mainly includes a full generalized regular expressions support, can describe any kind of automaton and has been made easier to support. We redesigned the Vaucanson XML parser structure to get rid of a bad management of dependencies. It is updated according to the rfc. +
Nous avions commencé l'année dernière à travailler sur une nouvelle proposition de format XML de description d'automates, devenu FSMXML. Nous présentons cette année une version aboutie de ce travail sous forme de rfc. FSMXML comprend notamment une gestion complète des expressions rationnelles généralisées, il permet de décrire n'importe quel type d'automate et sa gestion est facilitée. Nous avons repensé la structure du parseur XML de Vaucanson pour s'affranchir d'une mauvaise gestion de dépendances et l'avons mise à jour conformément à la rfc. +
Vaucanson is a finite-state machine manipulation platform for automata and transducers. The version 2.0 is, today, in active development and has a new core with static and dynamic layers. In Vaucanson 1.4, the input/output was managed by a XML format specified by the Vaucanson Group: FSMXML. My work consisted in refreshing and developing these specifications. Now with this update, FSMXML can be used to save and load automata with specific Weight Sets like rational expressions or even weighted automata. +
Vaucanson est une bibliothèque de manipulation d'automates et de transducteurs. La version 2.0 est aujourd'hui en cours de développement et le design a été revu pour avoir des parties statiques et dynamiques. Dans Vaucanson 1.4, les entrées/sorties utilisent intensivement le format XML spécifié par le groupe de Vaucanson, FSMXML. Mes travaux consistent à développer et rafraîchir des spécifications du format présent dans Vaucanson 1.4. Cette mise à jour nous permet la sauvegarde et la lecture d'automates aux Weight Sets particuliers tels que des expressions rationnelles ou même des automates pondérés. +
Image registration is a process widely used in image processing. Considering two measurements '"`UNIQ--math-00000009-QINU`"' and '"`UNIQ--math-0000000A-QINU`"' of the same object (say, a radiography and an magnetic resonance image (MRI)), this technique estimates a transformation of '"`UNIQ--math-0000000B-QINU`"' so that the object in '"`UNIQ--math-0000000C-QINU`"' becomes aligned with the object in '"`UNIQ--math-0000000D-QINU`"'. Basically this technique is able to superimpose the image '"`UNIQ--math-0000000E-QINU`"' over the image '"`UNIQ--math-0000000F-QINU`"', allowing the client to see mixed information. This presentation will discuss the implementation of a fast image registration algorithm in Milena, the Cxx generic image processing library from the Olena platform, developed at LRDE. Specific techniques used to improve this process will be introduced. +
The Fast Level Line Transform (FLLT) constructs a contrast-invariant representation of an image. This algorithm builds a tree which follows the inclusion of the shapes contained in an image. For an image filter, having the contrast-invariant property is interesting. For instance, in the field of document image analysis, this representation is precious to extract characters whatever their mean gray-levels are brighter or darker than their surroundings. This document presents how this algorithm is introduced in our image processing library and shows the results of some connected that can be derived from this representation. +
The '"`UNIQ--math-00000002-QINU`"'-automata, capable of modeling infinite behavior, are used in numerous domains including model checking. The algorithms used are in general very costly. For this reason, we want to reduce the automata size while preserving the recognized language by applying numerous reductions. This report, in the continuation of the previous one, we will presents some improvements to the simulation based reduction and a new algorithm: the path refinement. +
The '"`UNIQ--math-00000002-QINU`"'-automata, capable of modeling infinite behavior, are used in numerous domains including model checking. The algorithms used are in general very costly. For this reason, we want to reduce the automata size while preserving the recognized language by applying numerous reductions. One of them, based on simulation, is very slow. In this paper, we will how to speed up using algorithmic methods and parallelization. +
Image inpainting is the process of reconstructing part of an image in a visually plausible way. Its purpose is either to repair a damaged image or to remove an object such as superimposing text in a video. Many approaches have been proposed in order to deal with both small and large regions. However most of these being not adapted to real time applications, we propose a simpler method based on structure reconstruction and color diffusion in order to solve the problem with strong interest in performances. +
Le fictitious play, en théorie des jeux, est une règle d'apprentissage dans laquelle chaque joueur suppose que ses adversaires jouent une stratégie fixe (potentiellement mixte, c'est-à-dire une distribution de probabilité sur un ensemble de stratégies). À chaque tour, chaque joueur joue ainsi le meilleur coup contre la stratégie de ses adversaires, déterminée de manière empirique à partir de leurs coups précédents. La convergence de telles stratégies n'est pas assurée, mais on sait que si il y a convergence, alors les stratégies jouées correspondront statistiquement à un équilibre de Nash. Il est donc très intéressant de connaître les critères de convergence. Nous nous intéresserons pour cette présentation au cas des jeux où les fonctions d'utilité (le gain d'un joueur en fonction des stratégies jouées) de chaque joueur sont identiques. Nous étudierons d'abord des résultats de convergence dans ce cas particulier. Afin de réduire la complexité en temps, nous verrons une variante de cet algorithme, qui consiste à autoriser une erreur dans la meilleure réponse des joueurs. Nous présenterons enfin un exemple d'application du fictitious play pour résoudre un problème a priori non lié à la théorie des jeux : un problème d'optimisation, c'est-à-dire calculer le maximum des valeurs prises par une fonction. +
Les dernieres années ont été marquées par le développement des techniques de segmentation à base de filtres connectés. Ces méthodes procèdent généralement en deux étapes. Elles calculent un attribut sur les composantes connectées puis filtrent celles qui ne satisfont pas un certain critère. Nous proposons un nouvel algorithme basé sur l'union-find qui permet de calculer des attributs directement sur les contours des composantes connectées et d' en étudier leur energie. Nous introduisons ainsi le filtrage à base de contours dans une nouvelle méthode de segmentation. +
The problem of finding short synchronizing words is important and has many applications (part orientersroad-coloring problem, model-checking, biocomputingnetwork protocols etc.) A synchronizing word (or reset sequence) for a finite deterministic automaton is a sequence of labels which sends any state of the input automaton to a unique state. Finding the shortest synchronizing word for a general automata is NP-completeso most algorithms focus on trying to find heuristically short words in polynomial time. In this report, we will compare the different approaches used by the current state of the-art algorithms (Greedy, Cycle, SynchroP, SynchroPLand FastSynchro), in terms of space and time complexityand actual results (average lengths of found words, average time spent). We will also discuss the different intermediate representations used by these algorithms, and how we can use the information they contain. +
The current problem of the disambiguation in Transformers with attribute grammars is that no-one has a proof that allows certification of this approach. The current use of attribute grammars for the disambiguation of C and a part of C++ lets us think that this method is correct. In order to remove any doubt, a definition and a formalization of our approach are necessary. This work is split in two parts. The first one relates to the proof of the validity of the approach used in Transformers. The second one is devoted to the correction and the re-development of the existing tools according to the model defined. +
Le problème actuel de la désambiguïsation dans Transformers avec des grammaires attribuées est que l'on ne possède pas de preuve permettant de certifier cette approche. L'usage actuel des grammaires attribuées pour la désambiguïsation du C et d'une partie du C++ laisse à penser que cette méthode est correcte. Afin de supprimer tout doute, une définition et une formalisation de notre approche est nécessaire. Ce travail comporte est divisé en deux parties. La première porte sur la preuve de la validité de l'approche utilisée dans Transformers. La seconde est consacrée à la correction et au re-développement des outils existants suivant le modèle défini. +
Spot est une bibliothèque de model checking. Pour vérifier des modèles, Spot utilise un format d'entrée représentant des automates de Büchi généralisés basés sur les transitions (TGBA). Ce format est peu pratique pour des utilisateurs, par son manque d'abstraction et par la taille des automates à représenter, souvent composés de millions d'états. Promela (Process Meta-Language) est un langage de spécification de systèmes asynchrones, utilisé par le model checker Spin. Il permet de représenter des systèmes concurrents dans un langage impératif de haut niveau. Nous allons présenter plusieurs approches pour l'ajout d'un front-end Promela dans Spot, qui devront permettre une exploration à la volée du graphe d'états, afin d'éviter de conserver en mémoire tous les états. +
Universal Background Models combined with Gaussian Mixture Models (UBM - GMM) is a common approach to speaker verifcation systems. In general, we use diagonal covariance matrices. This simplification allows us to have faster training steps during speaker recognition. We will explore the case of full-covariance along with the additional complexity and the benefits in terms of speaker recognition performances. All experiments will be performed on NIST-SRE 2010 datasets. +
Olena is one of the most advanced image processing libraries in terms of genericity. It mainly comes from a different vision of the image notion composed of key concepts such as Windows, Accumulators, Dispatch by Traits and Morphers. We make a detailed description and explain how to implement them within Lisp. +
G
In speaker verification appplications, GMM models have an important place and have shown good perfomance. Actuallylinear discriminant methods using support vector machines (SVM) provide better results. We will focus on a linear disciminant system, the SVM-GLDS. Its uses statistics directly extracted from the speech features to define the recognition model without using Gaussian mixture models (GMMs). Weâll present and compare SVM-GLDS performance to SVM-GMM on NIST speaker evaluation tasks. +
FIXME +
FIXME +
go2pins est un outil utilisé pour interfacer un programme Go avec des outils de vérification formelle. À l'aide d'une série de transformations, un programme Go est compilé vers un programme au comportement identique, mais exposant une interface permettant d'itérer l'espace d'états de celui ci. Nous introduisons les transitions black-box, une technique efficace et évolutive pour gérer le runtime Go. Cette approche permet des abstractions facilesautomatiques et efficaces. Dans ce rapport, nous présentons le développement derrière l'introduction des transitions black-box dans textttgo2pins et les problèmes rencontrés. +
Ce rapport présente l'implémentation d'une fac con générique et performante pour générer des automates aléatoires pondérés. Pour ce faire, nous utilisons des relations déjà établies entre des ensembles connus et l'ensemble des DFA de taille n. En étendant ces relations dans le cas pondéré, nous généralisons l'algorithme présenté et nous montrons une implémentation dans la plateforme Vcsn. +
Dans ce rapport, on présente l'implémentation d'un algorithme efficace et générique de génération aléatoire d'expressions rationnelles pondérées, et d'expressions rationnelles à plusieurs bandes. Il supporte tous les types opérateurs, d'étiquettes et de poids présents dans Vcsn. Cet outil permet une meilleure couverture des tests. Nous présentons également une manière de générer des chemins aléatoires dans des automates pondérés. +
H
go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. We introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approachinspired from the hardware verification techniques, allows easy, automatic and efficient abstractions. In this reportwe introduce the development behind the introduction of the black-box transitions in textttgo2pins and the problems encountered. +
The structure extraction of a digitized document is based on the setup of a processing chain composed of elementary algorithms. The high-level document structure analysis will be based on this same processing chain but will consider other abstract information on the structure composition of the document, to get more clues on its structure. From those clues and from the structure data of the document, it is then possible to perform high-level analysis like identifying the reading direction, extract some specific elements or convert the document into another format. +
Un histogramme est une représentation de la distribution de données dans une image, par exemple des niveaux de gris ou des couleurs. Cette caractéristique essentielle doit être implémentée génériquement dans la bibliothèque Milena. Durant ce séminaire nous proposons d'enregistrer les données d'histogrammes dans des conteneurs d'images. Pour cela, nous avons besoin d'adapter la définition des types de valeurs. Plus spécifiquement, nous proposons d'augmenter les traits associés aux types de valeurs, d'ajouter de nouveaux types de valeurs utiles et de construire de nouvelles abstractions au-dessus. Enfin nous présenterons comment traiter des données circulaires comme les valeurs de teinte (encodées par des angles dans l'espace de couleurs HSL); dans ce cas "l'image histogramme" deviendrait aussi circulaire. +
A histogram is a representation of the distribution of data in an image, e.g., gray-levels or colors. This common tool is used for many applications and especially for classification purposes. This key-feature has to be generically implemented in the Milena library. In this seminar, we propose to store histogram data using an image container. To that aim, adapting the definition of value types is required. More specifically, we propose to augment the traits associated with value types, add some new useful value types, and design new abstractions over them. Last, we present how to deal with circular data, such as the "hue" values (encoded by angles in the HSL color space); in this case, the "histogram image" would become also circular. +
Le module de structures algébriques de VaucansonAlgebra, sert de base à la définition mathématique des automates finis. Cependant la modélisation actuelle est inexacte du point de vue théorique: les relations d'héritages entre certaines classes sont fausses (l'héritage entre les semi-anneaux et les monoïdes en est le parfait exemple). D'autre part, nous ne pouvons facilement l'étendre avec de nouvelles structures algébriques.newline Ainsi, afin de doter Algebra d'une plus grande granularité dans sa définition des concepts algébriques, il est nécessaire de retravailler sa structure globale en introduisant un système de hiérarchie par propriétés similaire à celui présenté dans SCOOP. En se basant sur les propriétés des opérateurs et des ensembles mathématiques pour définir la nature des structures algébriques, et non sur une hiérarchie de classes classique, nous pourrons nous permettre une spécialisation plus précise des algorithmes grâce à la garantie de propriétés sur ces structuresentraînant ainsi un gain de performance et d'expressivité important au cur de Vaucanson. +
Decision Diagrams are a family of data structures that represents huge data sets using a small amount of memory. These structures can be of fixed size (tuples), or varying size (lists, maps, ...), the DD handling being different for each one. Data Decision Diagrams and Set Decision Diagrams handle varying size data thanks to operations named homomorphisms. However, the definition of a correct operation can be hard because numerous errors hard to identify can happen. This seminar offers a presentation of an algorithms library that gives a more abstract view on handled data. This library contains the algorithms defined in "List" and "Map" modules from the Objective Caml standard library, allowing the user to focus on his specific problem. +
Les Diagrammes de Décision sont une famille de structures de données permettant de représenter avec peu de mémoire de grands ensembles de données. Ces structures peuvent être de taille fixe (un tuple) ou variable (une liste, un conteneur associatif, ldots), la manipulation du DD ne se faisant pas de la même manière. Les Data Decision Diagrams et Set Decision Diagrams manipulent des données de taille variable grâce à des opérations, les homomorphismes. Cependant la définition d'une opération correcte peut dérouter l'utilisateur, et passe souvent par de nombreuses erreursdifficiles identifier. Ce séminaire propose une bibliothèque dùalgorithmes fournissant une vue plus abstraite que les homomorphismes "bruts" des données manipulées, en reprenant les algorithmes définis dans les modules "List" et "Map" d'Objective Caml. L'utilisateur peut se concentrer sur les parties spécifiques à son problème. +
I
Actually, i-vector space is the most recurrent representation of speech information in speaker recognition systems. The scoring process is generally based on Cosine Distance (CD) or Probablistic Linear Distriminant Analysis (PLDA) methods. The aim of this work is to replace these approaches by a MultiLayer? Perceptron (MLP). The MLP showed good performances in nonlinear function approximation. The main idea is to find better functions than cosine scoring method. The performance of the MLP method will be compared with other methods such as CD, PLDA and Restricted Boltzmann Machines (RBM) method presented by Jean Luc. +
In this work we apply Convolutional Neural Networks to the task of speaker recognition. The CNN is used to approximate a measure of the distance between two i-vectors (representation of a speaker). Contrary to the commonly used cosine similarity measure, the function approximated by a CNN can be non-linear. The performance of this model will be compared to the ones of the Cosine Similarity measure and PLDA classification. +
Building a robust speaker recognition system needs very slow and complex algorithms. In this work, we propose a deep neural network to map a low dimensionnal ivector space based on less complex model into high dimensional ivector space. The system will be evaluated on speaker recognition task of NIST-SRE 2010 data. +
Ce rapport présente l'implémentation en C++ de l'algorithme ID décrit par Dana Angluin et al dans Polynomial Identification of omega-Automata. Il permet l'identification, ou l'apprentissage passifd'omega-langages réguliers et des omega-automates associés, dans un temps et une mémoire polynomiaux. C'est un travail préliminaire à l'étude de l'apprentissage actif d'omega-langages. Le code est disponible sur https://gitlab.lrde.epita.fr/cpape/ID +
Les botnets sont devenus la technique principale pour effectuer des attaques au sein d'un réseau. Ils ont été utilisés dans le passé pour voler des informations auprès d'une organisation ou envoyer des spams. Plus récemment, les attaquants s'en sont servis à des fins financières pour par exemple miner des bitcoins. Dans cette perspective, il est essentiel de détecter ces réseaux malicieux afin de défendre les intérêts des utilisateurs ou d'organisations. La recherche publique a souvent 'dté derrière la forte adaptation des attaquants aux systèmes de détections d'intrusions. Nos travaux consistent en l'utilisation de techniques d'apprentissage automatiques non-supervisées encore inexplorées dans ce domaine afin de détecter différents types de botnets. +
Botnets are the primary way of attacking computer networks and are being used to steal information, spy organizations or send spams, by compromising devices connected to the internet. More recently, botnets have also seen themselves being used for financial interests such as mining bitcoins at a large scale. It is a primary threat which is essential to identify in order to defend the interests of users and any type of organization. Unfortunately, public research has often been one step behind the fast adaptation of attackers to detection systems. Our work consists in using unsupervised machine learning techniques unprecedentedly used on such tasks to detect botnets on different scenarios. +
Morphological operators can be applied on grayscale images to filter out some objects or conversely to emphasize some objects. Therefore, by choosing an appropriate structuring element, it is possible to eliminate some elements of a map like text and to reconstruct discontinuous lines. A filter bench has been defined to extract from images of ancient maps the thin lines whatever their orientation, that isthe plot boundaries. On the resulting images, a watershed algorithm can afterwards segment the plots. Moreoverapplying a "seam carving" algorithm as pre-processing removes grid lines when needed. +
As part of a partnership with the Gustave Roussy Institutthe LRDE's image processing library Milena, offers an application dedicated to image reconstruction. Different images of the same object but obtained from different modalities have to be processed. First, these images are simplified. Then objects contained by these images are extracted. The final step is to mix information into a unique image. Thereby, the process is composed of several stages: image filtering, segmentation, binarizationmultimodal image registration and image reconstruction. The presentation will especially focus on the segmentation part. +
Milena is the generic image processing library of the Olena platform. The library aims at remaining simple while providing high performances. The introduction of new image types based on graphs has revealed some design problems limit ing its genericity. For instance, we have always considered that "images have points"; yet some images have sites that are not points (but edges, facets, and even sets of points). Another erroneous assumption was to consider that sites are localized by a vector (e.g., (x,y) in the 2D plane), which cannot be true when sites are not point-wise. Therefore there was a need to reconsider the image types and their underlying images properties.In this seminar, we will present a new image taxonomy that solves those issues. +
FIXME +
FIXME +
In the model checking field, Partial Order Reduction (POR) is a method which allows to notably reduce the size of datastructures used to represent the different possible executions of program model, by considering only representative execution paths, insteed of all. This has a cost: information is lost. When the goal is only to check the absence of deadlocks, enough information is kept, so POR works well. But when in comes to LTL model checkingrelevent information may be dropped: execution paths which modifiy the value of AP (Atomic Proposition) occuring in the LTL formula. Moreover, it is only possible to use POR for LTL X. Invisible and transparent transitions are methods which add additional conditions to fulfill during the POR, in order to keep all execution paths which may modify the value of the AP. We explain these methods and how they have been implemented in the Spot model checking library. +
La morphologie mathématique est devenu un outil indispensable pour une bibliotheque de traitement d'image. Les algorithmes produit grace a cette technique sont tres efficaces et permettent des résultats tres satisfaisant notamment pour des opérations de segmentation d'image. Le travail produit a donc pour objectif d'implémenter et d'intégrer dans la bibliotheque Pylene les représentations hiérarchique morphologique. Notre travail s'est concentré principalement sur la pipeline globale de segmentation utilisant ces méthodes, ainsi que la visualisation grace aux cartes de saillance. L'objectif etant bien entendu de réaliser les algorithmes les plus optimisés possible pour pouvoir les utiliser sur de grandes images. +
The Common Lisp language provides a predicate functionSUBTYPEP, for instrospecting sub-type relationship. In some situations, and given the type system of this languageknowing whether a type is a sub-type of another would require enumerating all the element of that type, possibly an infinite number of them. Because of that, SUBTYPEP is allowed to return the two values (NIL NIL), indicating that it couldn't answer the question. Common Lisp implementations have a tendency to frequently not answereven in situations where they could. Such an abusive behavior prevents potential optimizations to occur, or even leads to violating the standard. In his paper entitled “A Decision Procedure for Common Lisp's SUBTYPEP Predicate”Henry Baker proposes an algorithm that he claims to be both more accurate and more efficient than the average SUBTYPEP implementation. We present here the current state the current state of our implementation and discuss one potential improvement based on R-trees of Baker's algorithm. +
The Common Lisp language provides a predicate functionSUBTYPEP, for instrospecting sub-type relationship. In some situations, and given the type system of this languageknowing whether a type is a sub-type of another would require enumerating all the element of that type, possibly an infinite number of them. Because of that, SUBTYPEP is allowed to return the two values (NIL NIL), indicating that it couldn't answer the question. Common Lisp implementations have a tendency to frequently not answereven in situations where they could. Such an abusive behavior prevents potential optimizations to occur, or even leads to violating the standard. In his paper entitled “A Decision Procedure for Common Lisp's SUBTYPEP Predicate”Henry Baker proposes an algorithm that he claims to be both more accurate and more efficient than the average SUBTYPEP implementation. We present here the current state the current state of our implementation and discuss one potential improvement based on R-trees of Baker's algorithm. +
C++ classes are closed, such that once a class definition is ended, nothing can be added to it. But most of the timeprogrammers are used to distinguish method definition from method implementation. As a consequence, using fully-qualified name of method names and return types are needed, which is repetitive and tedious, especially with template and nested classes. We propose extending C++ grammar with a namespace-like syntax in order to define easily member functions and static data members already declared in the class definition. This work will be based on Tranformers' C++ grammar and transformation rules in Stratego Language. +
Vaucanson is a finite state machine manipulation platform for automata and transducers. Usage highlighted the overly complex interface for the automaton manipulation. For the past two years, active development has been undertaken to introduce the concept of automaton kind. Today, a part of the new interface have been implemented and the work on the core of still Vaucanson 1.4 in a instable state. Firstthis report show the work done for Vaucanson 1.4, then on the work undertaken to make Vaucanson 2.0 stable. +
Les classes en C++ sont fermées, c'est-à-dire qu'on ne peut rien leur ajouter une fois leur définition terminée. Or, la plupart du temps, les programmeurs séparent la définition de l'implémentation, ce qui oblige à utiliser une syntaxe répétitive, en particulier dans le cas de patrons de classes ou de classes imbriquées. On se propose donc de faire une extension de la grammaire du C++ permettant via une syntaxe proche de celle des namespaces de définir plus aisément des méthodes ou attributs statiques déjà déclarés dans la définition de la classe. Dans ce but, nous utiliserons la grammaire du C++ implémentée dans Transformers, et des transformations écrites en Stratego. +
Le langage Common Lisp fournit un prédicat, SUBTYPEPqui permet d'introspecter la relation de sous-typage. Dans certaines situations, étant donné le système de typage du langage, il est impossible de déterminer si un type est un sous-type d'un autre sans en énumérer tous les éléments, possiblement en nombre infini. À cause de cela, SUBTYPEP est autorisé à retourner deux valeurs (NIL, NIL), indiquant qu'il n'a pas pu trouver de réponse. Les implémentations de cette fonction ont trop souvent tendance à ne pas répondre, même dans des situations où c'est théoriquement possible. Ce comportement abusif peut alors empêcher certaines optimisations potentielles du compilateur, voire même rendre l'implémentation non conforme au standard. Dans son article og A Decision Procedure for Common Lisp's SUBTYPEP Predicate fg, Henry Baker propose un algorithme qu'il prétend plus précis et plus performant que l'implémentation moyenne de SUBTYPEP. Nous présentons ici l'état de notre implémentation de l'algorithme de Baker ainsi qu'une potentielle amélioration de celui-ci faisant usage des R-trees. +
Le langage Common Lisp fournit un prédicat, SUBTYPEPqui permet d'introspecter la relation de sous-typage. Dans certaines situations, étant donné le système de typage du langage, il est impossible de déterminer si un type est un sous-type d'un autre sans en énumérer tous les éléments, possiblement en nombre infini. À cause de cela, SUBTYPEP est autorisé à retourner deux valeurs (NIL, NIL), indiquant qu'il n'a pas pu trouver de réponse. Les implémentations de cette fonction ont trop souvent tendance à ne pas répondre, même dans des situations où c'est théoriquement possible. Ce comportement abusif peut alors empêcher certaines optimisations potentielles du compilateur, voire même rendre l'implémentation non conforme au standard. Dans son article og A Decision Procedure for Common Lisp's SUBTYPEP Predicate fg, Henry Baker propose un algorithme qu'il prétend plus précis et plus performant que l'implémentation moyenne de SUBTYPEP. Nous présentons ici l'état de notre implémentation de l'algorithme de Baker ainsi qu'une potentielle amélioration de celui-ci faisant usage des R-trees. +
Dans le domaine de la vérification de modèle, la Réduction d'Ordre Partiel (ROP) est une méthode qui permet de réduire notablement la taille des structures de données utilisées pour représenter les différentes exécutions possibles d'un modèle de programme, en considérant seulement les exécutions représentatives. Cela a un coût : de l'information est perdue. Si le but est seulement de vérifier l'absence d'interblocage, il reste assez d'information. Mais en ce qui concerne la vérification de formules LTL, de l'information importante peut-être perdue : les exécutions qui peuvent modifier la valeur de PA (Propositions Atomiques) qui apparaissent dans la formule LTL. De plus, il est seulement possible de vérifier des formules LTL X. Les méthodes des transitions invisibles et transparentes ajoutent des conditions à remplir pendant la ROP, pour garder assez d'information pour la vérification de formule LTL. Nous expliquons le fonctionnement de ces méthodes et leurs implémentations dans la bibliothèque de vérification de modèles Spot. +
Vaucanson est une plateforme de manipulation d'automates finis et de transducteurs dont l'interface s'est montrée trop complexe. Pendant les deux dernières années, des travaux ont été entrepris afin d'introduire le concept de kind d'un automate dans la bibliothèque. Aujourd'huiune partie de la nouvelle interface a été implementée et le travail sur le cœur a laissé Vaucanson 1.4 dans un état instable. Cette présentation montrera dans un premier temps le travail effectué pour Vaucanson 1.4puis sur les travaux entrepris afin de rendre stable Vaucanson 2.0. +
In model checking using '"`UNIQ--math-0000003B-QINU`"'-automata, the construction of smaller automata reduces a lot the runtime and the memory consumption of costly operations such as the synchronized product. As the minimization of deterministic Büchi automata is an NP-complete problem, we focus our work on reduction operations. Spot already implements a method of reduction by simulation working with all existential automata with any type of acceptance. This method uses a one-step simulation based on the signatures of the states. L. Clemente and R. Mayr propose a reduction by '"`UNIQ--math-0000003C-QINU`"'-step simulation only working with Büchi automata and show that increasing this number of steps may improve the reduction. We try to generalize the existing reduction operation in Spot to make it work with signature-based '"`UNIQ--math-0000003D-QINU`"'-step simulations. We also present how we can extend the existing reduction to make it work with alternating automata. +
Computing optical flow has many applications including motion estimation, or as a first step towards video inpainting. The optical flow equation can not be solved as such due to the aperture problem (two unknowns for one single equation). One set of algorithms tries to solve this equation based on a global strategy, which is, trying to have small variations in the flow. The first of them is Horn-Schunck. This algorithm, even though it globally works, has several drawbacks, including being slow and unable to find large displacements. In order to solve those problems, many strategies have been developed. We will present the method and analyze the benefits of a multi-layer strategy applied to Horn-Schunck. +