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. +
One part of an OCR toolchain is to classify detected characters: they can be lowercase or capital letters, or digits. To do so, our OCR computes for each image of character an associated wavelet-based descriptor. This descriptor can then be classified. The classification step is currently based on a multiclass k-NN classifier. Since the testing step heavily depends on the number of samples of the training set, the latter can be modified to improve the scores. Our work is focused on the possible improvements of the training set. +
Vaucanson is a library aimed at providing easy access and manipulation of common automata constructions and their algorithms. As such it provides schoolbook algorithms (and some others on the bleeding edge) such as determinizationaccessible states calculation and so on. One of them is composition of transducers. This algorithm isn't from an obvious kind and his implementation in Vaucanson is perfectible. Improving such an algorithm implementation is consequently a good way to challenge Vaucanson design choices. +
Spot is a model checking library developed at the LRDE. Its strengh is to be based on Transition Based generalized Büchi Automaton (TGBA), instead of Transition Based Büchi Automaton (TBA) widely used in other model checkers. TGBAs allows us to create a very small automaton representing a given formula hence making the whole model checking process faster. Spot emphasizes on the usability and customization of its tools, a great concern is to be able to interface Spot with other programs. Degeneralization the process of transforming a TGBA into a TBA, is central in this view. We present in this report an analysis of the tools already present in Spot for degeneralization and we proposes some way to improve them. +
Safra's algorithm is a well known construction method which produces a deterministic Rabin automaton from a non-deterministic Büchi automaton. A variant of this method creates deterministic automata with a parity acceptance. However, these methods produce automata with '"`UNIQ--math-00000005-QINU`"' states. There already exist improvements that help reduce the number of states in many cases. In this paper we present two new strategies to help construct smaller deterministic automata. The first strategy uses the strongly connected components and tracks a different Safra run for each of these components separately. The second strategy uses the information that bisimulation gives us to help remove redundant states. This enables us to avoid searching multiples paths which are equivalent and hence reduces the final number of states. We show how these two strategies help reduce the resulting automaton and prove their correctness. We also provide some benchmarks to show that the resulting automata are almost always smaller. Finally, we compare our results to a tool called ltl2dstar which converts LTL formula to deterministic Rabin automaton. +
L'inpainting consiste à réparer des parties d'une image de façon visuellement plausible. Son but peut être de réparer des régions endommagées, ou de supprimer des objets tels que du texte superposé à une vidéo. De nombreuses approches ont été proposées pour répondre au problème dans le cas de petites ou de larges régions. Cependant la plupart d'entre elles ne sont pas adaptées à des applications en temps réel. Nous proposons une méthode plus simple basée sur la reconstruction de structure et la diffusion des couleurs afin de répondre au problème dans une optique de temps réel. +
L'inpainting consiste à réparer des parties d'une image de façon visuellement plausible. Une catégorie de méthodes répondant à ce problème est basée sur des équations aux dérivées partielles (EDP). Cette approche consiste à propager itérativement des informations géométriques et d'intensités à l'intérieur des régions à réparer. Cependant l'élaboration de tels modèles demande une compréhension théorique du processus de diffusion souvent difficile à obtenir. Basé sur le papier de Risheng Liu traitant d'une approche ascendante à la composition de l'EDP par combinaison d'invariants simplesnous proposons une mise en uvre optimisée que nous comparons à l'existant. +
Image Segmentation is the process of identifying the outline of objects in the composition of an image. In recent years, the use of Deep Convolutional Neural Networks for the purpose of Image Segmentation has spiked, with results outperforming more classical approaches. We will explore the implementation and potential applications of integrating filters from the theory of Mathematical Morphology within the structure of a Deep Convolutional Neural Network. +
Tiger is a language designed as a reference for pedagogical compiler writing. Our C++ implementation of a Tiger compiler takes advantage of well-established practices in program transformation tools. The multi-core era has made parallelization a requirement in any computer science curriculum. As a support for teaching, our compiler has to evolve and make use of modern parallel techniques. This report introduces a solution to distribute work in a task-based concurrency model using Intel Threading Building Blocks (TBB) to decouple the programming from hardware specificities. +
Image processing is a very broad field of study that encompasses a multitude of operations, each of them with different purposes and circumstances of use, complexities and results. Nowadays, the bests results for automatic image study (image segmentation, image classificationobject detection, etc.) are obtained using deep learningand more specifically convolutional neural networks. We explore and conduct experiments on a specific part of image processing, mathematical morphology, investigating on the best way of circumventing operations' complexities regarding their integration in a supervised learning pipeline. +
A timed automaton is an '"`UNIQ--math-00000003-QINU`"'-automaton which describe a model containing continue time conditions. Without treatments, those automata can have an infinite states space. However, we can translate them in finite automatacalled zone graph, to analyze their properties. In this report, we show how the timed automata have been integrated at Spot. We use TChecker, a program created at the LaBRI. We explain then how we integrate the representation of those TChecker's zone graph in Spot. Then we show how Spot's algorithms can read this translation to work on timed automata and zone graphes. We then explain how inconvenients of TChecker have been adapted to make simpler its utilisation by Spot. +
Pictures have noise and to reduce it, some algorithms are applied. One of them is the NL-Mean algorithm, implemented as a patch-based strategy. The main idea is to denoise a local region based on other similar neighboring patches. A spatial metric (the Euclidian distance) is used to determine the similarity between patches. The main objective of this project is to incorporate the information related to the statistical distribution of colors within a patch, thanks to the use of histograms, to potentially highlight characteristics that have been missed with the standard strategy. It may give some interesting information which could be helpful to improve picture denoising. This method adds robustness regarding any transformation which does not affect the shape of histograms (overall change of luminance or rotation) and can allow the use of patches which could have been discarded by the standard strategyafter proper post-processing of the patch. +
Vaucanson est une plateforme de manipulation d'automates finis. Débuté en 2002, le projet attire de plus en plus d'utilisateurs. De ce fait, une interface utilisateur efficace est nécessaire.par Pour l'utilisateur non expert, la manipulation d'automates peut s'effectuer via taf-kit, une suite d'outils accessible en ligne de commande. Une première interface graphique avait été esquissée en 2005, mais son fonctionnement était lent et compliqué car elle s'appuyait sur taf-kit pour réaliser chaque opération.par Cette nouvelle interface graphique, branchée directement sur le cur de la bibliothèque pour plus d'efficacité, simplifie la manipulation d'automates et rend accessible les algorithmes génériques de Vaucanson. +
Les images ont du bruit et pour le réduire, certains algorithmes sont appliqués. L'un d'entre eux est l'algorithme NL-Mean et qui se base sur une stratégie de patchs. L'idée principale est de débruiter une région locale en se basant sur d'autres régions similaires. Une métrique spatiale (la distance euclidienne) est utilisée pour déterminer la similarité entre les régions. L'objectif principal de ce projet est d'incorporer l'information liée à la distribution statistique des couleurs grâce à l'utilisation d'histogrammes, pour potentiellement mettre en valeur des caractéristiques qui n'ont pas été prises en compte dans la stratégie standard. Cela peut fournir des informations intéressantes qui pourraient être utiles pour améliorer la qualité du débruitage. Cette méthode ajoute de la robustesse en ce qui concerne toute transformation qui n'affecte pas la forme des histogrammes et peut permettre l'utilisation de régions qui auraient pu ne pas être prise en compte, en effectuant un post-traitement approprié de la région. +
Un automate temporisé est un ω-automate représentant un modèle comportant des conditions de temps continu, ce qui peut aboutir à un espace d'états infini. Cependant, il est possible de le ramener à un automate fini, appelé graphe de zones, afin d'étudier ses propriétés. Dans ce rapport, nous montrons comment les automates temporisés sont intégrés à Spot. Nous utilisons TChecker, qui est un programme conc cu au LaBRI. Nous expliquons comment sont intégrés les représentations des graphes de zones qu'utilise TChecker pour travailler sur les automates temporisés dans Spot. Nous montrons ensuite comment les algorithmes de Spot lisent cette adaptation pour travailler sur des automates temporisés et des graphes de zones. Nous montrons enfin comment sont contournés certains inconvénients de TChecker afin de rendre plus simple son utilisation par Spot. +
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. +
Tiger est un langage utilisé à des fins pédagogiques dans l'étude des compilateurs. Écrite en C++, notre implémentation d'un compilateur Tiger profite de techniques éprouvées dans la transformation de programmes. L'ère du multi-cur a rendu la parallélisation indispensable dans le cursus d'un étudiant en informatique. Utilisé comme support de cours, notre compilateur doit évoluer et tirer profit des nouvelles techniques de parallélisme. Ce rapport présente une solution pour distribuer le travail au sein d'un modèle de programmation concurrente par tâche. Nous utiliserons Intel Threading Building Blocks pour nous détacher des problématiques matérielles. +
Text in document images that is subject to extraction through document analysis can be present in two forms: dark text over light background (conventional form) or light text over dark background (Inverse Video). This report introduces the problematic of extracting inverse video text using an existing toolchain, its integration in Scribo, the problems it involves and solutions to better results that we have explored. +
Le traitement d'image est un domaine d'étude très vaste qui englobe une multitude d'opérations, chacune ayant des spécificités, des circonstances d'utilisation, des meilleurs résultats pour l'étude automatique des images complexités et des résultats différents. Aujourd'hui, les meilleurs résultats pour l'étude automatique des images (segmentation d'imagesclassification d'images, détection des objets, etc.) sont obtenus en utilisant l'apprentissage profond, et plus spécifiquement les réseaux neuronaux convolutifs. Nous explorons et menons des expériences sur une partie spécifique du traitement d'image, la morphologie mathématique, en recherchant la meilleure façon de contourner les complexités des opérations concernant leur intégration dans un pipeline d'apprentissage supervisé. +
K
Lorsque l'on cherche à obtenir plusieurs plus courts chemins d'un graphe, il n'est pas intéressant de lancer plusieurs fois un algorithme de plus court chemin puisqu'il retournerait toujours le même chemin. Plusieurs algorithmes existent pour pallier ce problème. L'un d'eux, l'algorithme de Yen, cache des transitions dans le graphe entre chaque calcul de plus court chemin. Ce travail présentera l'implementation de cet algorithme dans Vcsn ainsi que les différentes techniques d'optimisations envisagées (notamment l'implementation d'un ensemble creux). +
Le calcul des K plus courts chemins dans un automate peut être très coûteux, surtout sur des automates énormes comme ceux utilisés en linguistique. Ainsiaprès avoir implémenté l'une des solutions considérée comme l'état de l'art (appelée l'algorithme de Yen) dans Vcsn, l'étape suivante était l'implémentation de la meilleure solution pour ce calcul sur des automates avec des cycles: Eppstein. Ce travail va décrire nos différentes implementations et comparer leurs performances. +
When trying to retrieve multiple shortest paths in a graph, we cannot simply run a shortest path algorithm multiple times as it would always retrieve the same. Some algorithms exist to solve this problem. One of them, the Yen algorithm hides transitions in the graph between each calculation to retrieve the correct paths. This work will present how it was implemented in Vcsn and the optimization techniques we tried on this algorithm (including the implementation of a sparse set). +
The K shortest paths computation can be very time consuming especially when applied to the enormous automata used in linguistics. Hence, after having implemented one of the state-of-the-art solution to the problem (namely Yen's algorithm) in Vcsn, the next step was to implement the best known solution for automata with cycles: Eppstein. This work will describe our different implementations and compare their performances. +
L
L'arbre de partition binaire est, en traitement d'imagesune structure qui permet la segmentation et la recherche efficace d'information dans une image. Il peut être créé à partir de différents modèles de région et fonctions de calcul de distance entre ces régions. La construction de cet arbre se fait habituellement à partir d'une image pré-segmentée pour des questions de performance et de gain de temps. La sensibilité de l'arbre au bruit dans l'image peut aussi être étudiée, pour trouver par exemple quels niveaux de l'arbre sont influencés par ce dernier. +
L'algorithme Union-Find de Tarjan (TUFA) produit, à partir d'une image, un arbre reprèsentant des classes d'èquivalences dans une image ètant donnèe une relation. Cette reprèsentation peut être utilisèe pour dèfinir des filtres. Cette mèthode est actuellement utilisèe dans Milena, notre bibliothèque de traitement d'image, pour implèmenter des filtres connectès comme par exemple l'ouverture et la fermeture d'aire, de volume ou encore de hauteur. Ces filtres sont utilisès pour filtrer une image tout en prèservant les contours. Cette propriètè est un avantage par rapport à l'ouverture et la fermeture basèes sur l'èrosion et la dilatation. TUFA peut être utilisè par des algorithmes conservant les domaines disjoints, ce qui est un second avantage intèressant. Ce document prèsente une mèthode pour implèmenter une sèrie de nouveaux filtres, notamment auto duaux. +
La représentation des i-vectors dans le cadre de la locution représente l'état de l'art dans le domaine de la vérification du locuteur. Grâce à des méthodes d'apprentissage supervisé (la Distance Cosinus avec l'Analyse Discriminante Linéaire et la méthode de Covariance intra-classe), des progrès significatifs ont été réalisés dans ce domaine. Cependant, de récentes recherches proposent d'utiliser une base de données non étiquetées d'i-vectors, afin d'augmenter la taille de l'ensemble des données d'entraînement et de réduire le coût de constitution de cette base. C'est pourquoi nous basons notre étude sur l'espace des i-vectors, et travaillons ainsi avec des méthodes d'apprentissage non supervisé. Dans cette étude, nous utilisons une méthode de partitionnement, le processus de Markov Clustering (MCL), afin de regrouper de façon naturelle les i-vectors qui représentent un même locuteur dans un ensemble d'entités. L'algorithme MCL est un algorithme de partitionnement non supervisé rapide et extensible, basé sur la simulation de flux stochastiques dans les graphes. Le résultat du partitionnement est utilisé dans le système supervisé standard de vérification du locuteur pour évaluer les performances. Nous allons aussi comparer celle-ci avec d'autres méthodes de regroupement comme l'Infomap, le Self-Organizing Map et Newman-Girvan. +
We present a new tool for circuit synthesis from LTL specifications. It reduces the synthesis problem to a parity game using Spot's efficient algorithms on '"`UNIQ--math-00000003-QINU`"'-automata. Two methods have been implemented for the resolution of the game: a recent algorithm by Calude et al. which has the best known theoretical complexity for the problem, and Zielonka's recursive algorithm known for its good practical performances. Finally, the winning strategy is translated to an And-Inverter Graph that models the original LTL formula. +
La séparation du locuteur est un sujet important dans le domaine de la recherche. Il s'agit de savoir qui parle à quel moment dans un enregistrement audio, c'est-à-dire que nous aimerions connaître les intervalles de temps durant lesquels chaque locuteur parle. En calculant les Coefficients Cepstraux sur l'échelle de Mel (MFCC) de notre enregistrement audio, et en utilisant l'Analyse en Composantes Principales (ICA), nous pouvons avec l'aide de chaînes de Markov cachées (HMM), segmenter l'enregistrement. Nous utiliserons cet algorithme pour la segmentation du locuteur dans le système de vérification du locuteur, avec des enregistrements audio où plusieurs personnes parlent, comme dans les enregistrements d'entretiens ou bien les enregistrements microphone de l'évaluation de reconnaissance du locuteur de NIST. +
Ces dernières années, de nombreuses recherches ont été faîtes sur la séparation de sources audio. Lors de réunions ou dans des lieux publics bruyants, il arrive souvent que plusieurs personnes parlent en même temps. Ainsi, chaque voix doit être extraîte des audio en contenant plusieurs, afin d'être correctement reconnue. Un algorithme efficace pour ceci est celui de l'Analyse en Composantes Indépendantes (ACI). L'ACI modélise un mélange de signaux comme une forme standard de superposition linéaire des signaux sources. Même dans des conditions environnementales difficiles, le résultat de l'ACI contiendra toujours de fortes composantes résiduelles du mélange de voix. Nous allons utiliser cet algorithme pour la segmentation du locuteur dans le système de vérification du locuteur. Nous obtiendrons de meilleurs résultats, particulièrement dans le cas de données audio avec plusieurs orateurs, comme dans les interviews ou les enregistrements de microphones de l'évaluation de reconnaissance du locuteur de NIST. +
Le model checking est un domaine de la vérification formelle permettant de vérifier le comportement d'un système à travers des formules logiques. Spot est une bibliothèque de model checking qui repose sur une des techniques du domaine : l'approche automate. Dans cette approche du model checking, le système et les formules sont représentés sous forme d'automates acceptant des mots de longueur infinie, et plus particulièrement des automates de Büchi. Spot propose de nombreux algorithmes aux utilisateurs de la bibliothèque pour manipuler ce type d'automates, en vue d'applications au model checking. Pourtant, un algorithme est manquant : celui de la complémentation d'automates de Büchi (qui produit un automate reconnaissant la négation du langage initialement reconnu). Cet algorithme est peu utilisé dans la pratique à cause de sa forte complexité, mais il ne manque pas d'intérêt du point de vue théorique. Nous présenterons une implémentation d'un tel algorithme dans Spot. +
Le model checking est un domaine de la vérification formelle, qui permet de vérifier le comportement d'un système avec l'aide de formules logiques temporelles. Spot est une bibliothèque de model checking qui repose sur une des techniques du domaine : l'approche automate. Dans cette approche du model checking, le système et les formules sont représentés sous forme d'automates acceptant des mots de longueur infinie, et plus particulièrement des automates de Büchi. Spot propose de nombreux algorithmes aux utilisateurs de la bibliothèque pour manipuler ce type d'automates, en vue d'applications au model checking. Une opération sur ces automates a récemment été ajoutée dans Spot : la complémentation. La recherche d'algorithmes effectuant cette opération est toujours d'actualité puisqu'il n'existe toujours pas d'algorithme atteignant les bornes théoriques optimales. Nous présenterons deux algorithmes récents de complémentation que nous venons d'ajouter dans Spot, qui se basent sur des automates alternants. +
La généricité par propriétés est un paradigme qui étend la programmation orientée objet et l'adapte à certains systèmes pathologiques. Elle a été introduite au LRDE par le paradigme orienté C++ SCOOP. Le principe est de caractériser une classe par les propriétés de ses instances au lieu de ses relations d'héritage. Nous présenterons ce paradigme et montrerons qu'il peut être utilisé indépendamment du langage et du domaine d'application. Nous introduirons ensuite un exemple d'implémentation en Common Lisp. +
La programmation orientée contexte est un paradigme permettant de prendre en compte les problématiques transverses et les variations de comportement d'un programme dépendantes du contexte. Ce paradigme permet ainsi d'exprimer des aspects du comportement d'un programme qui sont orthogonaux à sa modélisation objet, tout en maintenant son abstraction et sa modularité. Dans le domaine du traitement d'images, par exemple, la programmation orientée contexte peut être utilisée pour prendre en compte des aspects qui traitent à la fois de la structure de l'image, de son contenu, ou encore sa représentation mémoire. Nous présentons la programmation orientée contexte, puis nous analysons ensuite les problématiques transverses présentes dans Climb, une bibliothèque de traitement d'images écrite en Common Lisp. Nous expliquons ensuite comment la programmation orientée contexte permet de résoudre ces problématiques. Enfin, nous analysons les avantages de la programmation orientée contexte dans le domaine du traitement d'images. +
Les automates alternants ajoutent un branchement universel au branchement existentiel des automates non-déterministes. Les automates alternants de Büchi sont exponentiellement plus concis que les automates de Büchi non-déterministes. De plus, ils conviennent bien à la traduction de la logique temporelle linéaire car leur taille est proportionnelle à la taille de la formule traduite. Ce travail vise à ajouter le support des automates alternants à Spot. Cela rendra Spot compatible avec les outils produisant et utilisant des automates alternants, et permettra à de futurs algorithmes travaillant sur les automates alternants d'être implémentés. +
Image Segmentation is the process of identifying the outline of objects in the composition of an image. In recent years, the use of Deep Convolutional Neural Networks for the purpose of Image Segmentation has spiked, with results outperforming more classical approaches. We will explore the implementation and potential applications of integrating filters from the theory of Mathematical Morphology within the structure of a Deep Convolutional Neural Network. +
L'espace Total Variability (TV) représente actuellement l'état de l'art dans le domaine de la vérification du locuteur. Des progrès significatifs ont été réalisés grâce aux nouvelles méthodes de classification comme l'Analyse discriminante linéaire probabiliste (PLDA) ou la Distance Cosinus (CD). Dans cette étude, nous explorons une nouvelle méthode pour déterminer la distance entre deux i-vecteurs en utilisant une variante des Machines de Boltzmann, ces nouvelles approches ont montré des résultats satisfaisants dans le domaine du traitement d'images. Nous allons aussi comparer les performances en terme de fiabilité avec les méthodes classiques comme PLDA ou CD. +
La détection des formes et la reconnaissance d'objets font partie des enjeux les plus importants du traitement d'images. Différentes stratégies ont déjà vu le jour; néanmoins celle basée sur l'utilisation des arbres de composantes semble particulièrement prometteuse. En effet, l'arbre de composantes permet d'établir puis de mettre en relation les composantes à différents niveaux de gris de l'image. À partir de cet arbre, il devient alors possible d'appliquer des attributs qui serviront de critères pour filtrer ces composantes et mettre en évidence les objets de l'image. Nous présenterons donc l'implémentation de ces arbresl'utilisation des attributs et des politiques de propagation pour filtrer les composantes, ainsi que la chaîne de traitement qui permettra d'identifier ces objets. +
Jusqu'à présent, Vaucanson s'adressait essentiellement à la communauté des automaticiens. Cependant, il existe d'autres domaines où les automates sont utilisés. Dans ce rapport prospectif, nous nous orienterons vers la communauté des linguistes et, plus précisément, vers le domaine du traitement automatique des langues naturelles car les besoins de ce domaine diffèrent de nos utilisations habituelles. Nous observerons diverses spécialités et dresserons un bilan des besoins en automates. Ainsi, nous pourrons évaluer l'adéquation de Vaucanson pour ce domaine et en dégager des pistes d'évolutions éventuelles pour le projet. +
Avoir de hautes performances tout en conservant la généricité est un des domaines de recherche prépondérant au sein du LRDE. Milena, la bibliothèque de la plate-forme Olena, confronte ce problème au domaine du traitement d'image. De plus, Milena a aussi pour objectif de rester simple à utiliser. Une solution à ces problèmes, utilisée depuis plusieurs annéesrepose sur les propriétés. Les propriétés sont un ensemble de caractéristiques associées statiquement à un type particulier. Par exemple, les types d'images de Milena possèdent une propriété speed qui indique les temps d'accès aux valeurs des images. Durant ce séminaire, nous nous intéresserons aux propriétés des types d'images. Nous détaillerons les définitions de ces propriétées. Nous montrerons aussi comment les propriétés aident à améliorer les performances tout en maintenant la généricité. Pour cela, nous prendrons en illustration l'implémentation des routines bas niveau dans la bibliothèque. +
La famille des relations rationnelles synchrones est la plus grande famille de relations rationnelles, définie jusqu'ici, qui est une algèbre de Boole effective. Fournir des outils permettant de les manipuler peut donc s'avérer intéressant pour leur étude. Le récent support des alphabets de paires dans Vaucanson nous permet une nouvelle approche pour travailler avec les relations rationnelles synchrones, représentées par des transducteurs lettre à lettre, pour lesquels nous fournissons les outils nécessaires à leur manipulation. +
Le projet Olena fournit une bibliothèque générique pour le traitement d'images, Milena. Nous voulons que cette bibliothèque procure de nombreux types de valeur tels que l'utilisateur puisse toujours choisir le type adapté pour son application. Par exemple, nous fournissons de nombreux encodages en niveau de gris, de nombreux espaces de couleur, etc. Nous présentons la manière dont nous mettons en uvre les types de couleurs dans Milena. Il existe différents espaces de couleur (RGB, HSI, et bien d'autres) et il existe plusieurs encodages possibles pour les mêmes espaces de couleur (rgb_3x8, rgb_f, etc.). Nous voulons rendre les choses plus faciles pour l'utilisateur. Donc, notre objectif est de rendre possible l'utilisation des espaces de couleur sans se soucier des mécanismes internes. Par exemple, dans les formules de conversion, on ne veut pas faire apparaître les détails d'implémentation (division par 255). +
Segmenter une image consiste à en extraire les régions d'intérêt, par exemple pour séparer des cellules cancéreuses en imagerie médicale. L'approche par transformation de la ligne de partage des eaux (LPE) ou Watershed Transform permet d'obtenir une telle segmentation. Il en existe de nombreuses définitionsainsi que diverses implémentations, dont certaines sont à la fois performantes et produisent un résultat avec de bonnes propriétés, comme le emphTopological Watershed. Cet exposé présentera l'implémentation d'un algorithme calculant cette LPE au sein de Milena, la bibliothèque C++ générique de traitement d'image de la plate-forme Olena, développée au LRDE. Nous nous intéresserons tout d'abord aux formats d'images “classiques”, puis à la généralisation à des formats d'images plus inhabituels (images à support de graphe généraux, etc.). +
Currently, i-vectors become the standard representation of speech context in speaker and language recognition method. Cosine Distance (CD) is the most popular scoring method. It uses Linear Discriminant Analysis (LDA) and Within Class Covariance Normalization (WCCN) to reduce the channel variabilities. The aim of this work is to reduce channel variabilities locally before applying the CD. The idea is to create a large i-vector graph from a training dataset. After clustering it with community detection algorithmsthe target and the test i-vectors are projected into this graph. Only their neighborhood are selected to train the LDA and WCCN. Results will be compared with the global channel compensated method. +
The detection of logotypes and invariants inside an image aims to find within an image (or a sequence of images) a new or already known graphical element which pertains to a brand, a company, somebody, etc. Such elements could be found in many real-life pictures but also in advertising pictures. The detection challenge is to compare elements with those which have been already seen but also to set up a machine learning approach in order to determine if there are new logotypes. The integration of such a tool inside the Olena image processing platform and possibly inside the Terra Rush project could lead to a better content indexing and to invalidate specific areas in other processing toolchains. In this report, we will mainly explain a generic method to locate invariants keypoints of an image : the SIFT descriptor. +
Discriminating factor detection inside images is a very active area of research in computer vision. Current applications are widely used, from robotic to assisted digital photography. Our presentation will be focused on logotype detection from natural images. Using Olena, an open-sourced, generic and efficient image processing platform, we have implemented our own SIFT descriptor detector. +
Training a convolutional neural network relies on the use of loss functions, which provide an evaluation of the performance that allows the network's optimisation. Different loss functions evaluate performance in different ways, and thus affect the training differently. This report aims to share our progress in evaluating the performance of various loss functions in the training of convolutional neural networks for brain tumour segmentation. +
M
Les og packages fg de Common Lisp offrent une fonctionnalité analogue aux espaces de noms présents dans des langages comme le C++. Ceux-ci permettent d'encapsuler des symboles qui peuvent être exportés ou privés. Les symboles exportés doivent être explicitement déclarés lors de la définition du package. Cette liste de symboles est fastidieuse à maintenir lors du développement de projets de grosse envergure. Dans ce rapport, nous étudions des techniques de maintenance automatiques de cette liste. Plusieurs alternatives sont présentées et comparées. +
La mise au point d'un système de reconaissance du locuteur performant nécessite l'utilisation d'algorithmes complexes et lents. Cette publication propose l'utilisation d'un réseau neuronal profond afin de mapper un espace d'ivecteur de faible dimensionnalité fournis par un modèle simple vers un espace d'ivecteur de forte dimensionnalité. Ce système sera evalué à la reconnaissance du locuteur sur les données de NIST-SRE 2010. +
The i-vector speech context representation became the state of the art in speaker verification. We had significant progress in this challenge with supervised methods (Cosine Distance with Linear Discriminante Analysis and Within Class Covariance method). However, the recent researches propose to use unlabeled data set of i-vectors to increase the size of training dataset and decrease the cost of collected data. This is why we base our study on the i-vectors space and work on unsupervised methods. In this study, we use a clustering method, the Markov Clustering process (MCL), to recognize natural groups of i-vectors which represent one speaker, within a class of entities. The MCL algorithm is a fast and scalable unsupervised cluster algorithm based on simulation of stochastic flow in graphs. The clustering result is used in the standard supervised speaker recognition system to evaluate the performances. We will compare these performances with other graph clustering methods, such as the Infomap, Self-Organizing Map and Newman-Girvan. +
Mathematical morphology is a classical method of image segmentation. In the past few years, maching learning using deep fully convolutional networks provides started providing extremly good results. We thus introduce morphological operators in those networks in order to improve their performance. +
Ce rapport résume trois méthodes implémentées dans l'outil de vérification de modèles Spot. La première vise à améliorer la conversion de modèle de programme en structure de Kripke grâce à la réduction d'ordre partiel, une technique qui ignore l'ordre de certaines actions du programme. Cela permet de réduire la taille de la structure de Kripke. La seconde méthode modifie la première pour permettre de l'utiliser pour tester des propriétés LTL. La troisième a pour but de vérifier qu'un modèle ne contient pas de livelock, sans utiliser de propriété LTL. Nous testons toutes ces méthodesen se concentrant sur leur but commun : réduire la quantité de mémoire requise, ce qui est un goulot d'étranglement important dans le domaine de la vérification de modèles. +
This work uses a siamese architecture to learn a similarity measure. We apply two different samples over two identical sub-networks with the same set of weights. The input of each network is based on statistical information of speech data. We can then compute the distance between both informations. The DNN is able to reduce the dimensionality of the input because it learns an invariant mapping. We present the results of the learned similarity metric using different kind of informations and compare them to classic metrics based on PLDA or cosine similarity applied to i-vectors. +
Le model checking est une discipline s'intéressant à la vérification automatique de la conformité d'un système fini vis-à-vis d'une propriété. Spot est une bibliothèque de model checking basée sur une approche automate: le système à vérifier est représenté par un automate de Büchi généralisé basé sur les transitions, les propriétés sont exprimées par des formules de logique temporelle linéaire (LTL) et sont traduites en automate de Büchi. Les formules LTL peuvent être classées dans une hiérarchie selon le type de propriété qu'elles représentent. Nous étudierons le cas des formules LTL représentant des propriétés d'obligation, ces formules peuvent être reconnues par un type plus précis d'automates dont il est possible de calculer une forme minimale canonique. +
Model checking is a research field addressing the automatic verification of the correctness of finite-state systems towards a specification. Spot is a model checking library based on an automata approach: the system is translated into a transition-based generalized Büchi automaton, the specifications are expressed as linear temporal logic (LTL) formulae and then translated into a Büchi automaton. LTL formulae can be classified into a hierarchy depending on the type of property they express. We will study the case of LTL formulae representing obligation properties. These can be recognized by a restricted class of automata which have a computable canonical minimal form. +
Model checking aims to verify that a system meets the given specification by exploring all its possible states. To achieve that, there are several techniques. The Multi-Core Nested Depth-First Search (CNDFS) has a low memory requirement and works well with the simplest Büchi automatons. The Multi-Core On-The-Fly SCC Decomposition (UFSCC) has a greater memory requirement and works well with generalized Büchi automatons. The Symbolic method has a lower memory requirement but depends a lot on the order of the variables. The performances of these algorithms can be very different and choosing the best one given a specific model without testing all of them is not something easy. Here, we are trying to use machine learning to predict the best method to use for a given model. For that purpose, we train a random forest, an ensemble learning method that uses a multitude of decision treesusing only the first states of the state space. +
There is evidence that many news items are covered by troll farm accounts (i.e. over biased opinion or “fake news” spreading accounts). By modelling techniques and finding patterns of those accounts, it would be possible to anticipate their actions, and inhibit the spread of rumors. Within this context, the goal is to build a model to flag such accounts on trending topics. To do so, we use an unsupervised approach based on a dataset full of trolls from different countries released by Twitter in 2019 +
Dans le domaine de la reconnaissance du locuteur, les réseaux de neurones profonds (DNN) ont récemment été montrés plus efficaces pour collecter des statistiques Baum-Welch utilisables pour l'extraction d'i-vector que les modèles de mélanges gaussiens traditionnels. Cependant, ce type d'architecture peut être trop lent au moment de l'évaluation, demandant l'utilisation d'un processeur graphique pour atteindre des performances "temps-réel". Nous montrons que les statistiques produites par un réseau de neurones à délai temporel (TDNN) peuvent être utilisées pour construire un GMM supervisé plus léger servant de modèle du monde (UBM) dans un système i-vector classique. L'erreur obtenue avec cette approche est comparée à celles obtenues avec des modèles du monde basés sur des GMM classiques. +
Le modèle du monde représenté par les mélanges de gaussiennes (UBM - GMM) est l'approche état de l'art pour les systèmes de vérification du locuteur. On utilise généralement des matrices de covariance diagonale. Cette simplification permet d'avoir un apprentissage rapide des différents modèles. Nous allons explorer le cas des matrices de covariance pleines. On va présenter la complexité additionelle et les gains en termes de performances. Toutes les experiences seront menées sur des données issues de NIST-SRE 2010. +
Des travaux récents ont mis en évidence la place des comptes troll-farm dans la propagation d'informations fausses ou fortement biaisées. En établissant un modèle de reconnaissance de ces comptes et en détectant leurs modes d'action, il serait possible d'anticiper la propagation de ces campagnes. Dans ce contexte, l'objectif est de bâtir un modèle de classification de ces comptes sur les sujets d'actualité. Pour cela, nous utilisons une approche par apprentissage non supervisé sur un jeu de données contenant des informations sur de nombreux comptes troll proposé par Twitter en 2019 +
La morphologie mathématique est une méthode classique de segmentation d'image. Récemment, l'apprentissage machine à l'aide de réseaux de neurones convolutionels profonds fournis des résultats de plus en plus intéressants. Nous introduisons donc des opérateurs morphologiques dans ces réseaux de manière à améliorer leurs performances. +
Les algorithmes morphologiques sont l'un des atouts majeurs de Milena, la bibliothèque de traitement d'image générique et performante développée au LRDE. En effet, ils sont très utiles et relativement peu implémentés dans les autres bibliothèques. Ces algorithmes requièrent des opérateurs de bornes supérieure et inférieure (supremum et infimum) qui n'existent pas par défaut pour des types composites comme les couleurs encodées en rouge-vert-bleu (RVB). Nous présentons donc une implémentation de ces opérateurs pour le type RVB ainsi que toute la chaîne de traitement permettant de faire fonctionner des algorithmes morphologiques sur des images en couleurs. +
This work takes place in the context of Milena, the C++ generic image processing library of the Olena platformdeveloped at LRDE. Morphological algorithms are one of Milena's major assets. Yet few image processing libraries implement them even though they are very useful. Those algorithms require supremum and infimum operators, which don't exist by default for composite types like red-green-blue (RGB) pixels. We therefore propose the implementation of those operators for RGB values, along with a complete toolchain allowing morphological algorithms to work on color images. +
The Morse-Smale complex is a useful tool to analyse the topology of an image. However, its computation is quite expensive, and several algorithms exist having some differences in the definition of the complex. On the other hand, the Watershed Cut is a morphological algorithm, which segments grayscale images. It considers that an image is an edge-weighted graph, where the weights are given by the image gradient. Lidija Comic was the first to coin a possible equivalence between the algorithms to compute the Morse-Smale complex and the Watershed Cut with specific markers on the minima and maxima of the image. In this work, we discuss about this possibility, and we propose an implementation of a modified Watershed Cut algorithm working on vertex-weighted graphs as a way to compute the Morse-Smale complex. +
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.newline Afin d'y arriver, l'interface fut refaite ainsi que la mécanique interne de Vaucanson. Ceci amena plusieurs changements dans les structures de données, les algorithmes et la définition de l'interface. Nous exposerons ces modifications tout en mettant en avant les divers pièges qu'un développeur pourrait rencontrer en travaillant dans le coeur de la bibliothèque. Ce travail pourra amener à des mesures de performances entre Vaucanson 2.0 et la dernière version stable de la bibliothèque. +
Plusieurs méthodes d'évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents, il est donc difficile d'estimer la pertinence de celles-ci. Afin d'évaluer ces méthodes, la solution proposée est de confronter les évaluations automatiques avec l'évaluation humaine en considérant celle-ci comme référence. Pour obtenir cette référence, un site internet à été réalisé de façon à ce qu'un grand nombre d'utilisateurs puissent classer de façon simple les résultats d'un grand nombre d'algorithmes de détection de texte sur des grandes bases d'images. L'interface utilisateur a été développée pour minimiser le nombre de comparaison que l'utilisateur doit réaliser afin d'obtenir un classement cohérent. Nous l'appliquerons sur les résultats du concours ICDAR 2013 (8 méthodes sur un lot de 233 images). +
Le model checking explicite de systèmes concurrents souffre d'une croissance exponentielle du nombre d'états représentant un système. Les méthodes de réduction par ordre partiel sont un ensemble de méthodes permettant de combattre ce problème. Celles-ci permettent d'ignorer les états redondants lors de la génération de l'espace d'états. Parmis elles, nous avons choisi les algorithmes two phase et ample set comme base pour nos investigations. Ceux-ci ont été implémentés dans Spot, la bibliothèque C++ de model checking développée au LRDE, en utilisant l'interface DiVine. En se basant sur ces méthodes et sur le fait que les algorithmes dans Spot sont calculés à la volée, nous avons défini une nouvelle classe de méthodes appelées méthodes de réduction par ordre partiel adaptatives. L'idée est de se baser sur l'état courant de l'automate de la formule et non sur la formule tout entière. Les résultats obtenus sur notre suite de tests montrent que cette méthode donne de meilleurs résultats que les méthodes d'ordre partiel classiques. +
Spot est une bibliothèque de model checking implémentant une approche par automates. Pour le moment les algorithmes de vérification de propriétés dans Spot utilisent l'espace d'états sans réduction du système. Ils souffrent donc de l'explosion combinatoire de la taille de ce dernier. Une manière de résoudre ce problème est d'utiliser des méthodes de réduction par ordre partiel. Ces méthodes permettent d'ignorer certains comportements équivalents du système pour une certaine propriété. Ainsi il est possible de réduire la taille de l'espace d'états généré tout en conservant le même comportement général. Le but de ce travail est d'évaluer comment ces méthodes d'ordre partiel peuvent être intégrées dans Spot. +
N
Vcsn is a platform dedicated to the creation and manipulation of finite state automata and transducers, with or without multiplicity. It provides a fast and efficient C++ library and a Python 3 binding. It also comes with a web-based interface in Python 3 (Jupyter) to ease the more complex use of the C++ interface. The goal of this work is to add new straightforward and pedagogic ways to interact with the library by adding smart features to the web-based interface. The user shall naturally and quickly access to the whole feature of the platform such as creating automata with different algorithms or drag and drop style and applying other algorithm on newly-created automata. +
SPOT is a C++ model checking library that relies on the automata theoretic approach to model checking. The first step of this approach consists in the translation of an LTL formula to an automaton that recognizes the same language. Currently, there exists two algorithms in SPOT that translate LTL formulæ to transition based generalized Büchi automata (TGBA). We want to implement a third translation for comparison. This new method translates the LTL formula into an alternating automaton, and then applies a nondeterminisation algorithm which takes as input the alternating automaton and gives out a TGBA. To complete this task, the alternating automaton structure will first be set up in SPOT, then the nondeterminization algorithm will be implemented, and last, the translation of LTL formulæ to alternating automata will be added. +
SPOT est une bibliothèque de model checking basée sur l'approche par automates et sur les automates de Büchi généralisés basés sur les transitions (TGBA) pour la vérification de systèmes exprimés sous forme de formules logiques. L'approche automate consiste à traduire une formule logique LTL en un automate qui reconnaît le même language. Dans l'état actuel des choses, il existe deux algorithmes dans SPOT de traduction de formules LTL vers des TGBA. Un troisième algorithme y sera rajouté. Ce dernier convertira dans un premier temps la formule LTL en un automate alternant, puis appliquera un algorithme de nondéterminisation sur celui-ci pour obtenir un TGBA. Le but de cette nouvelle implémentation est de mener une comparaison avec les deux autres déjà en place. Pour mener à bien cette tâche, la structure des automates alternants sera intégrée dans SPOT, puis ce sera au tour de l'algorithme de nondéterminisation d'automates alternants vers des TGBA et enfin la traduction de formules LTL sous forme d'automates alternants. +
The i-vector space is nowadays considered as the standard representation of speech information for speaker verification systems. This low dimensional representation of data along with new classifiers such as the Probabilistic Linear Discriminant Analysis (PLDA) or the Cosine Distance (CD) classifier have enabled new progress. The idea of the CD scoring classifier is to map higher dimensional features onto a lower dimensional hypersphere. All current systems first use a classical Linear Discriminant Analysis (LDA) to find the best projection to the lower dimensional space before actually projecting onto the hypersphere. The aim of this work is to define a non linear projection from the higher space directly to the lower dimensional hypersphere which minimizes the intra-class correlation while maximizing the inter-class correlation. The result should be compared to other solutions: Classical CD, PLDA, MultiLayer Perceptron approximation of distance measure and Restricted Bolzmann Machines. +
Spot est une bibliothèque de model checking centrée sur l'approche automate et qui permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur des modèles représentés par des automates de Büchi généralisés basés sur les transitions (TGBA). Spot propose actuellement trois algorithmes pour traduire des formules LTL en TGBA, une des étapes principales de l'approche automate. Nous présentons une quatrième traduction, introduite par Tauriainen, qui utilise des automates alternants basés sur les transitions (TAA) comme représentation intermédiaire. Nous le comparerons ensuite aux trois algorithmes déjà présent dans Spot. +
O
Context-Oriented programming is a promising paradigm for adressing the crosscutting concerns in software. This paradigm allows for the specialization of classes and methods based on context. Yet, it does not provide mechanisms for object coercion, that is, converting an object existing in a given context into another version for another context. We expose how this problem is an important lack in the paradigm, providing examples from Climb, an image processing library developped at the LRDE. We present solutions for automatic context-based object coercion, and we analyze them in terms of simplicity and genericity. +
Avec la diversification des moyens d'acquisitions (imagerie satellitaire, imagerie médicale, photographie HDR), les types d'images à traiter ne cessent de se multiplier (2d, 3d, etc..) créant le besoin d'algorithmes capables de traiter tous ces types. Pylene, une bibliothèque de traitement d'images, vise à apporter une solution simple et générique à ce problème grâce à l'apport d'interfaces de haut niveau. Néanmoins, une telle abstraction a souvent un cout et on doit faire un compromis entre une solution trop générique qui serait peu performante et une solution performante qui serait trop spécifique. De plus ces interfaces ne sont pas conformes aux récentes versions du standard ce qui limite sa facilité d'utilisation. Nous proposons ici une solution qui n'aurait pas à sacrifier la performance au détriment de la généricité. Cette solution s'appuie sur le concept de "range", introduit par Eric Niebler, que nous avons adapté aux besoins du traitement d'images et auquel nous proposons d'ajouter le nouveau concept de ranges segmentées. Il en découle un nouveau design qui réconcilie nos interfaces avec le nouveau standard pour tirer parti des nouvelles facilités syntaxiques, et qui de plus, offre un coût d'abstraction nul. +
Common Lisp est un langage de programmation dynamique. Bien qu'il ne soit pas a priori axé sur la performanceil s'avère que le langage offre certaines fonctionnalités liées à l'optimisation. Cependant, le gain en performance a un impact sur la généricité du code, l'optimisation limitant celle ci. Climb est une bibliothèque de traitement d'image écrite dans ce langage, ayant pour objectif de se comparer à des équivalents écrits dans des langages statiques tels que C++. L'objectif est de profiter de la généricité qu'offre Common Lisp pour l'écriture d'une bibliothèque de traitement d'image. Mais une telle bibliothèque a également des contraintes de performance, il s'agit donc de trouver un terrain d'entente entre ces deux aspects. Nous présenterons les différentes fonctionnalités qu'offre Common Lisp pour optimiser un programme, et leur utilisation dans Climb pour rendre la bibliothèque plus rapide, sans pour autant diminuer sa généricité. Nous présenterons également les premiers résultats du travail d'optimisation dans Climb, le travail restant et les apports de l'utilisation de Common Lisp pour une telle tâche. +
Le compilateur Tiger est un projet éducatif jouant un rôle central dans le cursus de la troisi`me année de l'EPITA. Ce projet est l'occasion d'enseigner aux étudiants des bonnes pratiques de développement logiciel comme les design patterns ainsi que l'importance des tests et de la documentation. L'ère de l'informatique séquentielle étant terminée, la programmation parallèle, autrefois releguée aux universités et aux laboratoires de recherche est maintenant devenue incontournable dans tout cursus d'informatique, pour cette raison nous aimerions introduire du parallèlisme dans le projet. Dans ce rapport nous étudions les possibilités de parallélisation dans le compilateur Tiger en utilisant la bibliothèque Intel Threading Building Blocks (TBB). Nous avons également diagnostiqué et corrigé plusieurs soucis de performance dans l'algorithme d'allocation de registres. +
Common Lisp is a dynamically typed language. Even if it is not a priori oriented towards performance, the language provides tools for optimization. Nevertheless, a gain of performance may have an impact on the genericity of the code, optimization limiting it. Climb is an image processing library written in Common Lisp, aiming to be compared with equivalents written in static languages, such as C++. The goal is to benefit from the genericity offered by Common Lisp for writing an image processing library. But such a library also has performance constraints. The goal is then to find a middle ground between those two aspects. We will present the different functionnalities that Common Lisp provides for optimization, and their use in Climb to make the library faster, without compromising the genericity of the library. We will also present the first results of this optimization work, the work that is left to be done, and the benefits of using Common Lisp for such a task. +
With the diversification of the acquisition devices (satellite imagery, medical imagery, HDR photography), the types of images to process has been steadily increasing (2d, 3d, etc...) thus the need for algorithms able to treat all these types. Pylene, an image processing library, aims to bring a simple and generic solution to this problem thanks to high level interfaces. However, such an abstraction often has a cost and we have to do a compromise between to a too gerenic solution which would be inefficient and an efficient solution which would be too specific. Moreover these interfaces are not compliant with the recent versions of the standard which limits his usage simplicity. We propose here a solution which would not has to sacrifice performance at the expense of genericity. This solution relies on the "range" concept, introduced by Eric Niebler, adapted to the image processing needs and to which we introduce the new concept of segmented ranges. It follows a new design which reconciles our interfaces with the new standard to take advantage of the new syntactic simplicity which features a zero cost overhead. +
The Tiger Compiler is an educative project playing a central role in EPITA's third year curriculum. This project is the opportunity to teach students software engineering practices such as design patterns, testing, documentationetc. As the age of serial computing is overparallel-computing technology that was once relegated to universities and research labs is now a core requirement in any computer science curriculum and thus we would like to introduce parallelization in the project. In this report we investigate the possibilities of parallelism in the Tiger Compiler using the Intel Threading Building Blocks (TBB) library. We also diagnosed and corrected several performance problems in the register allocation algorithm. +
SCRIBO, pour Semi-automatic and Collaborative Retrieval of Information Based on Ontologies, est un projet de dématérialisation ayant pour finalité la mise en place d'algorithmes visant à extraire des connaissances à partir de textes et d'images. Le redressement de l'image, en amont de la chaîne de traitements, est une phase nécessaire afin de corriger l'éventuel angle dû à la numérisation du document. De plus, l'extraction et l'étude des informations des caractères composant le texte permet non seulement de réaliser une reconstitution la plus fidèle possible du texte mais également de préparer ce dernier à son passage dans l'OCR. Ainsinous présenterons dans un premier temps un algorithme permettant de détecter l'inclinaison d'un document pour de petits angles, puis l'étude menée sur l'extraction des différentes caractéristiques des caractères. +
P
Climb is a generic image processing library written in Common Lisp. The library provides a low-level generic layer used to write image processing algorithms. In order to design processing chains, two options are currently available. One can either use a declarative Domain Specific Language or a GUI to specify the chain graphically. In order to improve the performance of the libraryparallelism can be introduced at those different levels. This presentation describes the various aspects of this parallelization process. For each level, we detail the implementation of the support for parallelism, its effect on the usability of the library and the achieved gain in performance. +
The tree of shapes is an useful image transform used to process digital images in a self-dual way. An (unpublished) algorithm working on '"`UNIQ--math-00000006-QINU`"'-dimensional cellular complexes allows us to compute a tree of shapes with a quasi-linear time complexity. However, due to the great number of cells added to the initial image, it is still usually slower than other '"`UNIQ--math-00000007-QINU`"' approaches specialized for 2D or 3D images. We present an approach to parallelize the quasi-linear algorithm in any dimension exhibiting interesting algorithmic and topological properties which can not be obtained from other approaches. The aim is to improve its computation time without breaking its theoretical complexity. +
Quicklisp is a library manager working with your existing Common Lisp implementation to download and install around 2000 libraries, from a central archive. Quickref, an application itself written in Common Lisp, generates automatically and by introspection, a technical documentation of every libraries of Quicklisp, and produce a website from this documentation. This technical report has a vocation to summarized the work performed until now on two aspect of this library. The first one is the parallelization of Quickref whereas the second one is the creation of three new indexes (by authorby keyword and by theme), requiring the implementation of text retrieval algorithms (lexical, semantic, etc...) +
Milena is an image processing library focused on genericity: using advanced template meta-programming techniques, algorithms are written once and can then run on many types of images: 1D, 2D, 3D, graph-based, built on a cell complex, etc. In order to improve the efficiency of the library we would like to introduce optimization techniques offered by modern processors: multicore parallelism and SIMD (Single Instruction, Multiple Data) vectorization. In this report we investigate how such low-level constructs can be integrated while preserving genericity. +
Milena est une bibliothèque de traitement d'images focalisée sur la généricité : en utilisant des techniques avancées de méta-programmation, les algorithmes sont écrits une seule fois et peuvent être ensuite exécutés sur de nombreux types d'images : 1D, 2D, 3D, sur une structure de graphe, sur un complexe cellulaire, etc. Afin d'améliorer les performances, nous souhaitons introduire des techniques d'optimisation rendues possibles par les fonctionnalités des processeurs récents: parallélisme multi-cur et vectorisation SIMD (Single Instruction, Multiple Data). Dans ce rapport nous étudions comment de telles fonctionnalités, à l'origine bas niveau, peuvent être intégrées tout en préservant la généricité. +
Climb est une bibliothèque de traitement d'image générique développée en Common Lisp. Elle fournit une couche de génécité bas-niveau utiliséee pour définir de nouveaux algorithmes de traitement d'image. Il est aussi possible de créer des chaînes de traitements soit en utilisant un "Domain Specific Language" déclaratif ou bien à l'aide d'une interface graphique. Afin d'améliorer les performances de la bibliothèqueces différents niveaux peuvent être parallélisés. Ce rapport technique décrit les différents aspects de ce processus de parallélisation. Pour chaque niveau, nous détaillons l'implémentation des traitements parallèles, leurs impacts sur l'utilisabilité de la bibliothèque ainsi que les gains de performance obtenus. +
Quickref est une application common lisp permettant de générer automatiquement et par introspection une documentation technique des bibliothéques disponibles dans Quicklisp. +
La bibliothèque Vaucanson permet de manipuler des automates et des transducteurs. Le parser d'expression rationnelles doit donc lui aussi traiter ces différentes structures. Malheureusement l'ancien parser ne permettait pas de lire des expressions rationnelles décrivant des transducteurs ou même des automates à poids autres que des nombres. Le nouveau parser permet de lire des expressions rationnelles contenant des poids de toutes sortes et des alphabets définis sur des produits de monoïdes. Ces différentes améliorations permettent d'interpréter des expressions rationnelles complexes représentant entre autres des transducteurs. +
FIXME +
FIXME +
Nowadays, model-checking tools suffer from a scalling problem, due to their memory consuption. Partial order reduction is one way allowing to notably reduce it, by computing only needed data on-the-fly. There are many state-of-the-art algorithms, and this method is used in many softwares (such as SPIN or LTSmin). We are going to talk about the implementation of it in the Spot libraryand then the optimisation. The results show a great decrease of the memory consuption, which implies some gain in all subsequent steps. +
Spot is a model checking library implementing an automaton based approach. For the moment to verify a property Spot's algorithm may explore the whole state space of the system without any reduction. They thus suffer from the combinatorial explosion in the model's size. One way to tackle this problem is by using Partial order reduction methods. The idea is to ignore equivalent behaviour of the system with respect to a given property. Hence, reducing the size of the generated state space while preserving the whole behaviour. The goal of this work is to assess how these methods can be implemented in Spot. +
The present report is the C++ implementation of the algorithm ID described by Dana Angluin and al in Polynomial Identification of omega-Automata. It allows identification, or passive learning, of regular omega-languages and omega-automata, in polynomial time and data. It is a preliminary work to the study of active learning of omega-languages. The code is available at https://gitlab.lrde.epita.fr/cpape/ID +
Prise de décision à l'aide de SVM dans le contexte des systèmes de vérification du loctueur à base d'I-Vector +
La prise de décision dans l'état de l'art des systèmes de vérification du locuteur est basée sur la distance en cosinus. Une approche différente est de considérer une prise de décision basée sur les Séparateur à Vaste Marge (SVM). La technique des SVMs a été largement exploitée dans la reconnaissance de formes et la prise de décision mais également en association avec les GMM super-vecteurs (GSV) en reconnaissance du locuteur. Cependant, l'idée d'utiliser les SVMs dans l'espace des i-vectors pour la reconnaissance du locuteur n'a pas été le sujet d'une étude approfondie. Nous étudierons les différentes fonctions kernels et comment c cela peut être utilisé dans la vérification du locuteur. Nous explorerons comment prendre en compte les variabilités de canal et de locuteur et dans l'espace des caractéristiques. Nous expérimenterons avec les données de la base NIST-SRE 2010. +
Spot, a library for transition based Spot, a library for transition-based '"`UNIQ--math-00000005-QINU`"'-automata manipulation, provides a method to determinize Büchi automata which can produce quasi-parity automata. We introduce three tools to manipulate these automata which are reducing the number of sets in the acceptance condition, changing the style of the parity acceptance expression and colorizing an automaton. Olivier Carton introduced a method to construct the product of state-based parity automata which keeps the parity acceptance. We adapt this method to make it work with transition-based automata and we present optimizations of this product. Our work gives a better support of automata with parity acceptance and may also lead to further optimizations of the determinization of Büchi automata. +
Spot, une bibliothèque manipulant les ω-automates basés sur les transitions, offre une méthode qui construit des automates à parité déterministes à partir d'automates de Büchi non-déterministes. Nous présentons trois outils qui manipulent les automates avec une condition d'acceptation à parité. Ces outils sont la réduction du nombre d'ensembles dans la condition d'acceptation, la modification du style de la condition d'acceptation et la coloration d'un automate. Olivier Carton a présenté une méthode pour constuire le produit d'automates à parité basés sur les étatsqui conserve la parité. Nous adaptons cette méthode afin qu'elle fonctionne également avec des automates basés sur les transitions, puis nous présentons des optimisations de ce produit. Notre travail offre un meilleur support des automates avec une conditions d'acceptation à parité. Il pourrait également permettre d'optimiser la déterminisation d'automates de Büchi. +
VAUCANSON is a finite state machine manipulation platform for automata and transducers. Usage highlighted the overly complex interface for the automaton manipulation. Therefore, work was done during the past years to improve it, leading to the introduction of the concept of automaton "kinds". Two different versions of the platform are currently under development. VAUCANSON 1.4, which will be a more complete and stable version of the work done before the interface modification. Idea is to work toward releasing a final version of VAUCANSON 1.X, allowing us to focus on VAUCANSON 2.0, which is currently incomplete, due to the deep changes that "kinds" brought to the library. This report will explain a new feature of VAUCANSON 1.4the Z/nZ semirings, and presents what has been and will be done to get VAUCANSON 2.0 to work. +
Projection non-linéaire pour l'attribution de score selon la distance en cosinus dans le contexte des systèmes de vérification du locuteur à base d'i-vectors. +
À l'heure actuelle, l'espace des i-vectors est considéré comme le modèle standard pour la représentation d'information vocale dans le contexte des systèmes de vérification du locuteur. De récents progrès ont pu être accomplis grâce à ce modèle qui permet de représenter les données dans un nombre réduit de dimensions et également grâce à l'utilisation de nouvelles méthodes de classification comme l'Analyse Discriminante Linéaire Probabiliste (PLDA) ou encore le classifieur à base de distance cosinus (CD). L'idée du scoring avec le CD est de projetter les caractéristiques évoluant dans un nombre de dimensions élevé sur une hypersphère de dimension plus faible. Aujourd'hui, tous les sytèmes utilisent d'abord une Analyse Discriminante Linéaire (LDA) classique afin de trouver la meilleure projection dans l'espace de dimension inférieure avant de projetter sur l'hypersphère. Le but de ce travail est de proposer une projection non linéaire directement de l'espace des i-vectors vers une hypersphère en minimisant la corrélation inter-classe tout en maximisant la corrélation intra-classe. Il sera question de comparer les résultats obtenus avec d'autres solutions comme : le CD classique, le PLDA et l'approximation de mesure de distance avec le perceptron multicouche et les machines de Bolzmann. +
Getting both high performance and genericity at the same time is one of the major research field at the LRDE. Milena, the Olena platform library, faces that issue in the context of image processing. Furthermore Milena has for extra objective to remain simple to use for a practitioner. A solution, experimented since several years, is based on properties. Properties are a set of features statically bound to a type. For instance, image types in Milena have a property named speed that gives information at compile time about the value access time. In this seminar, we focus on the image properties. We detail the definition of those properties and justify them. We show how those properties help in improving efficiency while maintaining genericity. For that, we take as illustration the implementation of low level routines in the library. +
In Vaucanson, Finite State Machines are mathematically defined by an algebraic structure module called Algebra. Considering the algebraic mathematical definitionshowever, the current design is inaccurate: some hierarchical relations are false (for example, the inheritance between semirings and monoids). Moreover, we are unable to add new algebraic structures easily.newline Therefore, in order to give Algebra more granularity in its algebraic concept definitions, it is necessary to rework its current structure by introducing a property based class hierarchy similar to the one presented in SCOOP. Using the mathematical operator and set properties to define algebraic structures, as opposed to a usual class hierarchy, we would be able to specialize algorithms more precisely thanks to structure property verifications, thus increasing Vaucanson's performance and expressiveness. +
Climb is a generic image processing library. A generic algorithm interface often requires several different specialized implementations. Olena, a C++ library, solved this using properties. We present a way to dispatch a function call to the best specialized implementation using properties in a dynamic programming language: Common Lisp. Then, we introduce examples of algorithms and properties used in image processing. +
Property-based genericity is an object-oriented programming paradigm. It allows to model in a generic way some systems which are hard to represent using classical object-oriented programming. It was introduced by the C++-oriented SCOOP paradigm used in Olena, an image processing library. The key principle of this paradigm is the description of classes in terms of a list of the properties its instances must have, instead of their inheritance trees.par We will present this paradigm and show that it can be extended to other languages than C++ and other fields than image processing. We will then introduce an example implementation of property-based genericity in Common Lisp, which will take advantage of its dynamic capabilities and its extensibility. +
Q
In this report, we show how the quotient operator has been implemented in Vcsn, a generic and perfomant automata manipulation library. After defining the left and right quotient over rational series, we explain the algorithm implemented in Vcsn to compute the quotient of two automata. We then explore the consequences of introducing the operator on the expression-side of the library, and particularly on expansions. +
Dans ce rapport, nous montrons comment le quotient a été implémenté dans Vcsn, une bibliothèque générique et performante de manipulation d'automates. Après avoir défini le quotient à gauche et à droite de séries rationnelles, nous expliquons l'algorithme implémenté dans Vcsn pour calculer le quotient de deux automates. Nous explorons ensuite les conséquences de l'introduction du quotient du côté des expressions dans la bibliothèque, et plus particulièrement sur les expansions. +
R
This report presents the implementation of an efficient and generic way to generate random weighted automata. To do so, we use a previously established relations between some known sets and the set of accessible DFA with n states. By extending these relations to the weighted case, we generalize the presented algorithm and we show an implementation in the Vcsn platform. +
In this report, we present the implementation of an efficient and generic algorithm to generate random weighted rational expressions, including multitape rational expressions. It support any operators, labels and weights present in Vcsn. This tool allows a better coverage for the tests. We also present a way to generate random paths on weighted automata. +
The Vaucanson library is designed to manipulate automata and transducers. Therefore we need a rational expression parser which deals with transducers. The current rational expression parser only takes as input weighted rational expression. The new parser allows us to specify any kind of weight and any kind of monoid like free monoid product. Both of these features are mandatory if we want to deal with transducers. The new parser is also less restrictive and provides more freedom to the user who can easily change the form of the grammar used to write its expression. +
... Insert an abstract in English here ... +
Le recalage d'images est une technique classique en traitement d'image. Soit A et B deux images représentant le même objet (par exemple une radiographie et une image à résonance magnétique (IRM)), on calcule une transformation de A telle que le recalage de l'objet dans A soit aligné sur l'objet dans B. Typiquement, cette technique peut permettre la lecture simultanée de deux mesures A et B. Cet exposé discutera des procédés de recalage rapide utilisés dans Milena, la bibliothèque C++ générique de traitement d'image de la plate-forme Olena, développée au LRDE. Certaines améliorations seront présentées. +
Dans un précédent rapport nous présentions le test de vacuité bi-bande dans la bibliothèque Spot, qui vérifie que l'intersection des langages de deux ω-automates est vide sans construire leur produitce qui permet de contourner une limitation de Spot sur le nombre d'ensembles d'acceptations de ces automates. Cette opération, lorsque l'intersection n'est effectivement pas vide, est généralement suivie d'une recherche de chemin acceptant sur le produit qui expose un mot qui se trouve dans les langages des deux automates. Nous présentons une nouvelle fonction qui réalise cette recherche de chemin acceptant à partir des données générées par le test de vacuité bi-bande, ce qui nous permet d'utiliser ces nouvelles méthodes dans des algorithmes qui nécessitent la recherche d'un contre-exemple. +
Le probléme de recherche de mots synchronisants les plus courts possible est un probléme important qui a beaucoup d'applications (orienteurs mécaniques, probléme de coloration de route, vérification de modélesbioinformatique, protocoles réseaux, etc.) Un mot synchronisant (ou une séquence de réinitialisation) pour un automate fini déterministe est une séquence d'étiquettes qui envoie n'importe quel état de l'automate d'entrée à un seul et même état. Trouver le plus court mot synchronisant dans un automate général est NP-complet, c'est pourquoi la plupart des algorithmes sont des heuristiques qui cherchent à trouver des mots les plus courts possible en temps polynomial. Dans ce rapport, nous comparerons les différentes approches utilisées par les algorithmes principaux les plus connus (Glouton, Cycle, SynchroP, SynchroPL et FastSynchro), en terme de complexité spatiale et temporelle, et les résultats empiriques (longueur moyenne des mots trouvés, temps utilisé par l'algorithme en moyenne). Nous discuterons aussi des différentes représentations intermédiaires utilisées par ces algorithmes, et comment utiliser les informations qu'elles contiennent. +
Spot est une bibliothèque de manipulation d'ω-automates qui tend à aider la vérification de modèle par ω-automates et le développement d'outils de transformation d'ω-automates. Elle fournit donc de multiples algorithmes avec de multiples implémentations qui fonctionnent sur une grande variété d'ω-automates. Parmi ces algorithmesles tests de vacuité et les recherches de contrexemple sont souvent utilisés pour de diverses raisons. Comme leurs résultats sont liés, ils sont souvent utilisés ensemble. Cependant, il manque à Spot les implémentations de recherche de contrexemple correspondant à certaines implémentations de tests de vacuité qui soient capables de travailler de la même manière sur les mêmes automates. Nous présentons deux implémentations de calcul de contrexemple, qui viennent compléter deux implémentations de tests de vacuité déjà existantes, qui suivent leur sillage et se servent des données dejà accumulées pour construire efficacement des contrexemples. +
Dans le cadre de son partenariat avec l'institut de cancérologie Gustave Roussy, Milena, la bibliothèque de traitement d'image du LRDE, propose une chaîne de traitement dédiée à la reconstruction d'image. Différentes images d'un même objet mais obtenues par différents modes d'acquisitions, sont traitées. Celles-ci sont d'abord simplifiées. On extrait ensuite les objets qu'elles contiennent. La dernière étape consiste à construire une image recoupant les informations des différentes images. Cette chaîne se décrit ainsi en plusieurs étapes : filtrage de l'imagesegmentation, binarisation, recalage d'image multimodales et reconstruction d'image. L'exposé se concentrera essentiellement sur l'etape de segmentation. +
Even if the accuracy of the text localization system developed by the laboratory has strongly increased, one main problem remains the speed. Indeed, the CPU and the memory resources used by the system need to be reduced if we want to be able to use it to extract text from video or embedded it in resource limited devices like smartphones. To achieve this goal, various methods to reduce the memory and CPU consumption can be used. However all of these methods do not give the same results according to the input image and some of them can decrease the accuracy of the final result. The target is to present these methods, their results, and analyze in what kind of situation they can be used. +
Un automate dèterministe peut être minimisè de manière efficace et donne un automate dont le nombre d'états est minimal. L'algorithme de réduction présenté dans ce rapport permet de construire un automate dont le nombre d'états est minimal à partir d'un automate non déterministe dont les poids sont définis sur un semi-anneau qui est un corps. L'algorithme calcule pour cela la base de l'espace vectoriel engendré par la série représenté par l'automate, ce qui permet de construire un automate dont le nombre d'états est égal à la dimension de cette base. L'algorithme se base sur la représentation matricielle des automates et nous amène à résoudre un système d'équations linéaires, ce qui force le semi-anneau de notre série à avoir les propriétés d'un corps. Nous voulons aussi que notre algorithme fonctionne sur des séries dont le semi-anneau est un corps non commutatif ce qui nous empêche d'utiliser les techniques classiques de résolution de systèmes linéaires. Ce rapport montre comment passer outre ces difficultés. Nous verrons enfin comment adapter notre algorithme pour qu'il fonctionne sur Z qui n'est pas un corps mais qui possède des propriétés suffisantes. +
FIXME +
FIXME +
Spot is a library of model checking algorithms which can manage different kinds of '"`UNIQ--math-00000003-QINU`"'-automata. It can also handle testing-automata since Spot 1.0. However, Spot 2.0 introduced a new data structure for automata with generic acceptance conditions that were not available when testing automata where developed. Our goal is to reimplement testing-automata using the more modern data structure. By doing so, we expect to reuse existing algorithms, to reduce the amount code specific to testing automata, and to make testing automata compatible with HOA format. Additionallyour preliminary implementation seems to produce smaller testing-automata than the original one. +
Vaucanson allows you to manipulate finite state machines. So the modeling of these objects 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. We will expose what can be considered as a Gordian knot in the actual modeling: for example Vaucanson is unable to choose the implementation of an automaton according to one of its properties. The proposed solution will reinstate a sane modeling and will prevent misconceptions while devising algorithm specifications. Finally, we will describe among other things a collection of specializations of the automaton concept and a set of improvements to the model that were previously too expensive to implement. +
Les réseaux de neurones profonds sont de plus en plus utilisés pour leur capacité à corréler des paramètres concrets afin d'en déduire des caractéristiques abstraites. Le réseau de neurones en goulot en est une forme particulière. Ce travail présente le fonctionnement de ce type de réseau et son utilisation pour le retraitement des Coefficients Cepstraux des Fréquences de Mel dans un système de reconnaissance du locuteur. Il est donc question d'étudier la convergence d'un tel réseau mais aussi la variation des performances du système en entier. +
L'arbre des formes est une transformée d'image utile pour les traitements d'images discrètes de façon auto-duale. Bien qu'il puisse être calculé grâce á plusieurs approches existantes dans la littératureaucune comparaison de ces algorithmes n'a été réalisée jusqu'á présent. Nous réalisons une comparaison de tous ces algorithmes du point de vue de leurs rapidités de calcul et de leurs occupations mémoire. Nous étu- dions aussi la parallélisation de l'algorithme quasi-linéaire et modifions les données qu'il manipule afin d'améliorer ses temps de calculs et son occupation mémoire. +
Program transformation in general purpose languages such as Cxx is tedious because it requires the ast of the transformed program to be manipulated in abstract syntax (that is, in the host language, Cxx here). The code to write is unwieldy and costly to maintain. This object of the seminar is to present the implementation of new concrete syntax program transformation techniques (that isusing directly the language of the transformed program) in a standard Cxx environment. Our approach uses the parser at run-time to apply dynamic transformation rules. A Tiger compiler will be used to support the presentation. +
La transformation de programmes dans des langages généralistes tels que le Cxx est fastidieuse car elle nécessite de manipuler l'ast du programme transform en syntaxe abstraite (c'est-à-dire dans le langage hôte, ici le Cxx). Le code à écrire est lourd et coûteux maintenir. Le but de ce séminaire est de présenter la mise en uvre de nouvelles techniques de transformation de programmes en syntaxe concrète (c'est-à-dire utilisant directement le langage du programme transformé) dans un environnement Cxx standard. Notre approche utilise l'analyseur syntaxique l'exécution pour appliquer des règles de transformation dynamiques. Un compilateur de Tiger servira de support à la présentation. +
Les ω-automates, capables de modéliser des comportements infinis, sont utilisés dans de nombreux domaines dont la vérification de modèle. Les algorithmes utilisés sont en général très coûteux. Pour cette raison, on veut réduire la taille des automates, tout en préservant le langage reconnu en appliquant de nombreuses réductions. L'une d'entre ellesbasée sur les simulations, est très lente. Dans ce rapport, nous allons montrer comment l'accélérer en utilisant des méthodes algorithmiques et de la parallélisation. +
Spot est une bibliothèque C++ de model checking utilisant l'approche par automates. Pour représenter les propriétés à vérifier, nous utilisons des formules LTL, qui sont traduites en automates. Dans Spot, ces automates sont des Automates de Büchi généralisés basés sur les transitions (TGBA). Un enjeu pour tout model checker, est d'être rapide. Une manière de faire est de rendre les automates aussi petit que possible. La littérature scientifique propose de nombreux algorithmes pour arriver à notre but. La bisimulation et la simulation réduisent des automates qui reconnaissent des mots de longueur infinis. Cette présentation montre comment adapter ces algorithmes pour des TGBA ainsi que le gain apporté par l'implémentation de la bisimulationce qui souligne l'importance d'implémenter la simulation pour réduire les TGBA. +
Les outils de vérification formelle souffrent actuellement d'un problième de passage á l'échelleà cause de leur consommation de mémoire. La réduction d'ordre partiel est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Il en existe beaucoup d'algorithmes à l'état de l'art, et cette technique est utilisée dans plusieurs logiciels (comme SPIN ou LTSmin). Nous allons parler ici de l'implémentation de certains de ces algorithmes dans la bibliothèque Spot, puis de leur optimisation. Les résultats obtenus montrent une diminution notable de la consommation de mémoire, ce qui implique un gain pour toutes les étapes suivantes de la vérification. +
Les ω-automates, capables de modéliser des comportements infinis, sont utilisés dans de nombreux domaines dont la vérification de modèle. Les algorithmes utilisés sont en général très coûteux. Pour cette raison, on veut réduire la taille des automates, tout en préservant le langage reconnu en appliquant de nombreuses réductions. Dans ce rapportdans la continuité du précédent, nous allons présenter de nouvelles améliorations à la réduction basée sur des simulations et un nouvel algorithme: le raffinement de chemin. +
L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Etessami et al. ont présenté une méthode de réduction d'un BA basée sur une relation de simulation (dite directe) entre ses états. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous montrons qu'en adaptant cette simulation aux TGBA on obtient des automates plus concis que les BA équivalents. Cette nouvelle technique est incluse dans Spot 0.9 et a permis de produire des automates plus petits que dans les précédentes versions. +
L'approche par automates du model checking s'appuie traditionnellement sur des Automates de Büchi (BA) qu'on souhaite les plus petits possible. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous avons déjà présenté une méthode de réduction par simulation (dite directe). Cette technique a permis de produire des automates plus petits que dans les précédentes versions. La simulation consiste à fusionner les états ayant le même suffixe infini. Nous montrons que nous pouvons aussi fusionner ceux ayant le même préfixe infini (c'est la cosimulation). On peut répéter la simulation et la cosimulation pour créer la simulation itérée. Cette méthode est incluse dans Spot 1.0 et est une grande amélioration de la simulation. On expérimente aussi une méthode qui consiste à modifier certaines conditions d'acceptations (appellées sans importances). Puisque celles qui sont sur les transitions entre composantes fortement connexes n'ont pas d'influence sur le langage, on peut les modifier pour aider la simulation. +
Même si la précision du système de localisation de texte développé par le laboratoire a aujourd'hui grandement augmenté, un des principaux problèmes demeure la vitesse. En effet, si l'on souhaite être en mesure de l'utiliser pour extraire du texte dans des vidéos ou s'il doit être embarqué dans des appareils aux ressources limitées tel que des téléphones portables, la consommation de ressources mémoire et CPU doit être réduite. Pour parvenir à cet objectifplusieurs méthodes permettant de réduire l'impact mémoire et CPU des étapes les plus coûteuses peuvent être utilisées. Cependant, toutes n'offrent pas les mêmes résultats en fonction de l'image d'entrée et certaines peuvent même dégrader le résultat final produit par le système. L'objectif est de présenter ces méthodes, d'observer leurs résultats et de déterminer dans quelles situations elles sont applicables. +
Spot peut gerer les automates testeurs depuis Spot 1.0. Cependant, Spot 2.0 introduit une nouvelle structure de données pour les automates avec des conditions d'acceptance génériques. Notre but est de réimplémenter les automates testeurs en utilisant cette nouvelle structure de données. Cela fait, nous espérons pouvoir réutiliser les algorithmes existants, réduire la quantité de code impliquant les automates testeurs et de rendre les automates testeurs compatibles avec le format HOA.L' implémentation choisis permettrait de reduire la taille des automates testeurs. +
S
Scool is a static object-oriented language. It has been created to help one to take advantage of all the power of static Cxx thanks to a more expressive syntax. It is not directly compiled but is translated into Cxx. This year was quite important for the project. Indeed, there are tight links between Scool's development and the generic image processing library Milena from the Olena platform. As some big changes occured in the library, work needs to be done to adapt the language to its new paradigms and to its new needs. Work also needs to be done to continue the implementation of the different features of Scool. This year the work will be focused on concept-oriented programming. This allows one to easily express constraints on generic programming. +
Cxx has proved to be a powerful language to write generic and efficient libraries. However using classical oo Cxx may not fulfill the efficiency criterion sought in some domains, e.g. when building scientific librarieswhere large data sets have to be processed through generic algorithms. A solution consists in combining the power of oop and emphstatic programming— which is in fact meta-code expressed thanks to Cxx template constructs. This has the advantage to replace the oo run-time overhead (due to virtual method dispatch) by compile-time computations. However, such an approach relies on code that is verbose, hard to write and to maintain. Though powerfulCxx lacks high-level static features, and thus clutters the semantics of static constructs with unrelated code. We present Scool, a static language mixing acoo and gp that has been created to take advantage of all the power of static Cxx thanks to a more expressive syntax and high-level constructs, without the drawbacks of plain Cxx. As a full-fledged static OOP language, Scool provides polymorphic methods (i.e., inclusion polymorphism), with the notable difference that every polymorphic call is statically-resolved: the design of Scool is based on the property that the exact (dynamic) type of every object is known at compile-time. As the aim of Scool is to bring all the power of static oop to Cxx, it is not directly compiled but translated into human-readable Cxx. The development of the translator raised classical problems found in dsl like traversal strategies of the abstract syntax tree. We propose an original solution based on the Stratego/XT program transformation framework, and some applications on Milena, a generic and efficient Cxx library from the Olena image processing platform. +
Le Cxx est un langage puissant pour écrire des bibliothèques génériques et performantes. Cependantdans certains domaines l'utilisation de l'orienté objet usuel peut poser des problèmes de performances, comme dans celui des bibliothèques de calcul scientifique dans lesquelles de grands ensembles de données parcourus par des algorithmes génériques. La solution proposée est la combinaison de la programmation orientée objet classique et de la programmation statique qui est en fait de la meta-programmation utilisant intensivement les templates du Cxx. Ceci a l'avantage de remplacer le coût à l'éxecution de l'orienté objet dû à la résolution des méthodes virtuelles par un coût `a la compilation. Cependant, cela engendre souvent du code verbeux, difficile à écrire et à maintenir. Malgré sa puissance, le Cxx ne possède pas d'abstractions statiques de haut niveau ce qui encombre la sémantique du code avec des détails d'implémentation. Nous vous présentons Scool, un langage statique fusionnant l'orienté objet et la programmation générique dans le but d'éxploiter toute la puissance du Cxx statique grâce à une syntaxe plus expressive. De plus, toutes les résolutions de méthodes se feront statiquement grâce au fait que le type exact (dynamique) de chaque objet est connu à la compilation. Le but de Scool étant d'apporter toute la puissance de l'orienté objet statique au Cxx, il ne sera pas directement compilé mais traduit en Cxx correctement formaté. Le développement du traducteur a soulevé les problèmes classiques du domaine des DSL comme la stratégie de parcours de l'arbre de syntaxe. Nous proposons une solution originale basée sur la plateforme de transformation de programme Stratego/XT avec des applications à Milena, la bibliothèque générique et performante de traitement d'image de la plateforme Olena. +
Scool est un langage statique orienté objet qui a été créé afin de pouvoir utiliser toute la puissance du Cxx statique de manière plus aisée grâce à une syntaxe plus expressive et agréable. Il n'a pas pour but d'être directement compilé mais d'être traduit en Cxx. Cette année le travail revêt une importance particulière. En effet, Scool est développé en étroite collaboration avec l'équipe de développement de la bibliothèque de traitement d'images Milena de la plate-forme textscOlena ; l'an passé a été pour elle le cadre de grands changements internes. Un des axes majeurs du développement de Scool va donc être de s'adapter aux nouveaux paradigmes et aux nouveaux besoins de la bibliothèque. Le second axe essentiel de travail est la poursuite du développement du langage. Cette année le travail va être concentré sur la programmation par concepts qui est une approche permettant de formaliser facilement des contraintes sur la programmation générique. +
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. In this report, we present a partial implementation of his algorithm, discuss some technical aspects, present some benchmarks and most importantlycompare the accuracy of both implementations. +
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. Dans ce rapport nous présentons une implémentation partielle de l'algorithme de Baker, nous exposons certains aspects techniques, nous présentons une étude des performances et enfin nous comparons l'acuité des différentes implémentations du prédicat. +
The best speaker verification systems are based on score combination of several approaches. Support Vector Machines (SVM) give very hopeful results. Thus, combining these methods could be very efficient. In our approach, we propose a new combination method for speaker verification systems based on SVM methods. This one performs a linear combination of several kernel functions in order to produce a new kernel function. In this combination, the weights are speaker dependent, by opposition of score combination approach for which the weight are universal. The idea is to adapt the combination weights for each speaker in order to take the advantage of the best kernel. In our experimentcombinations are performed on several kernel functions: the GLDS kernel, linear and Gaussian GMM supervector kernels. The method can use every kernel functions with no modification. The experiments are done on the NIST-SRE 2005 and 2006 (all trials) database. +
Les meilleurs systèmes de Verification du Locuteur (VL) sont fondés sur la fusion des scores de décision de plusieurs approches. Les méthodes basées sur les Séparateurs à Vaste Marge (SVM) donnent des résultats très performants. En conséquence, l'apport de ces méthodes est très important pour la fusion. Dans notre approche, nous proposons une nouvelle méthode de fusion des systèmes de VL basés sur les méthodes SVM en construisant une nouvelle fonction noyau à partir d'une combinaison linéaire de plusieurs fonctions. Dans cette combinaison, les poids utilisés varient selon les locuteurs, ce qui diffère des approches par fusion de score qui elles utilisent des poids universels. L'idée est donc de tirer avantage des performances de chacun des noyaux, et cela pour chaque locuteur donné. Ces combinaisons sont effectuées sur plusieurs types de noyaux dont les noyaux GLDS, GMM supervecteurs linéaires et Gaussiens. Les expériences sont réalisées sur la base des corpus NIST-SRE 2005 et 2006. +
State of the art speaker verification systems provide a decision based on cosine distance. A different approach is to consider a decision based on Support Vector Machine (SVM) separation. SVMs have been largely used in pattern recognition and decision making as well as in combination with GMM super-vectors (GSV). However, the idea of using SVMs in the i-vector space for speaker recognition has not been well explored. We will study the different kernel functions and how it could be used in speaker verification with i-vector space. We will explore how we could deal with channel and speaker variabilities in the feature space. The experiments are done on NIST-SRE 2010 core condition database. +
Afin d'améliorer la performance globale des systèmes de vérification du locuteur, il faut diversifier les approches. Le but de ce travail est d'étudier les performances d'un système SVM-MLLR. Cette méthode se base sur la construction, à partir du modèle du monded'une transformation linéaire des vecteurs moyennes (mean supervectors) maximisant la vraisemblance du modèle transformé par rapport aux données locuteur. On évaluera deux approches différentes : Dans la première, on utilisera directement le logarithme du rapport de vraisemblance (GMM-MLLR). Dans une deuxième expérimentation, on utilisera les SVMs pour évaluer les scores de décision. La dernière étape consiste à valuer l'apport d'une méthode de compensation du canal (NAP: Nuisance Attribute Projection) sur les performances de ce système). Une fusion des scores avec d'autres systèmes GMM sera étudiée. Une fusion au niveau des noyaux sera quand à elle présentée par Charles-Alban. Tous les tests vont être menés sur les deux bases de données NIST-SRE 2005 et 2006 all trials. +
Afin d'améliorer la performance globale des systèmes de vérification du locuteur, il faut diversifier les approches. Le but de ce travail est d'étudier les performances d'un système SVM-MLLR. Cette méthode se base sur la construction, à partir du modèle du monded'une transformation linéaire des vecteurs moyennes (mean supervectors) maximisant la vraisemblance du modèle transformé par rapport aux données locuteur. On évaluera deux approches différentes : Dans la première, on utilisera directement le logarithme du rapport de vraisemblance (GMM-MLLR). Dans une deuxième expérimentation, on utilisera les SVMs pour évaluer les scores de décision. La dernière étape consiste à valuer l'apport d'une méthode de compensation du canal (NAP: Nuisance Attribute Projection) sur les performances de ce système). Une fusion des scores avec d'autres systèmes GMM sera étudiée. Une fusion au niveau des noyaux sera quand à elle présentée par Charles-Alban. Tous les tests vont être menés sur les deux bases de données NIST-SRE 2005 et 2006 all trials. +
This report aims to explain and resolve a common problem that arise when handling inverse video (light color on dark background) : line collision. We will explain how to make a choice between two lines (one in inverse video, the other in normal mode) when they are superimposed by considering criteria and by balancing them. +
La fibrillation atriale est l'une des maladies cardiaque les plus communes, et peut être facilement détectée quand on peut localement détecter l'atrium du coeur dans une IRM. La segmentation manuelle demande un lourd travailet nous proposons ici une méthode de segmentation automatique, adapté d'une méthode développée pour la segmentation du cerveau humain. En utilisant l'apprentissage par transfert, nous réentrainons un réseau de neurone convolutionel con,cu pour la classification d'images naturelles, et nous constatons les avantages d'utiliser une technique de pseudo-3D. Nous explorons aussi des méthodes de prétraitement des données afin d'améliorer les résultats finaux. +
La detection des hyperintensites de la matiere blanche de facon efficace est un enjeu important dans le medical. Une detection efficace de ces dernieres permettrait notamment de mieux diagnostiquer certaines maladies neuro- degeneratives mais aussi déviter certaines erreurs medicales. Cést la problematique a laquelle nous avons tente de repondre dans ce rapport. On propose une solution se basant sur un reseau de neurones convolutif accompagne dún pretraitement effectue sur les entrees +
Le developpement du cerveau peut etre evalue grace a l'imagerie par resonance magnetique (IRM) du cerveau. Elle est utile en cas de naissance prematuree pour s'assurer qu'aucune maladie cerebrale ne se developpe pendant la periode postnatale. De telles maladies sont visibles sur un image IRM ponderee en T2 sous la forme d'hyperintensites de la matiere blanche. Pour evaluer la presence de ces hyperintensites, ce travail met en oeuvre une nouvelle implementation d'un outil, semi-automatique, base sur la morphologie mathematique, specialise dans la segmentation du cerveau des nouveau-nes. Nous passerons en revue les travaux connexes, l'implementation des differentes etapes et les difficultes rencontrees. Au final, la version developpee au cours de ce stage n'est pas completement terminee mais elle est en bonne voie pour une finalisation ulterieure. +
Les gliomes sont une catègorie de tumeur cérébrale ayant différentes formes et textures. La segmentation manuelle est complexe à cause de l'hétérogénéité de ces tumeurs. Plusieurs méthodes de segmentation automatique de gliomes ont été étudiées au challenge MICCAI 2018 BraTS, et nous voulons améliorer la soumission du LRDE, par l'utilisation d'opérateurs morphologiques, en gardant le même réseau de neurones et la “pseudo-3D”. +
Les gliomes sont une catègorie de tumeur cérébrale ayant différentes formes et textures. La segmentation manuelle est complexe à cause de l'hétérogénéité de ces tumeurs. Plusieurs méthodes de segmentation automatique de gliomes ont été étudiées au challenge MICCAI 2019 BraTS, et nous voulons améliorer la soumission du LRDE, par une compréhension plus approfondie de nos outils, et de nos données. +
Les gliomes sont une catègorie de tumeur cérébrale ayant différentes formes et textures. La segmentation manuelle est complexe à cause de l'hétérogénéité de ces tumeurs. Plusieurs méthodes de segmentation automatique de gliomes ont été étudiées au challenge MICCAI 2019 BraTS, et nous voulons améliorer la soumission du LRDE, par une amélioration de nos outils d'apprentissage. +
An elegant approach to manage ambiguous grammars consists in using a generalized LR parser which will not produce a parse tree but a parse forest. An additional step, called disambiguation, occurring just after the parsing, is then necessary. The disambiguation process consists in analyzing the parse forest to choose the only good parse tree using semantics rules. We use this approach in Transformers with the attribute grammars formalism. The lab work will be a comparison between this formalism and two other methods of disambiguation: the first one using ASF+SDF and the second one using Stratego language. The goal of this comparison will try to emphasize that attribute grammars are perfect to solve the disambiguation problem. Another thing will be to find the weakness of this method compared to the two others for a possible improvement of the system used in Transformers. +
Une approche élégante pour gérer les grammaires ambiguës consiste à utiliser un parseur LR généralisé qui produira non pas un arbre mais une forêt de parse. Une étape supplémentaire, appelée désambiguisation, survenant juste après le parsing, est alors nécessaire. Celle-ci consiste analyser cette forêt pour obtenir l'unique arbre valide correspondant à l'entrée en prenant en compte les règles de sémantiques contextuelles. C'est cette approche qui a ét retenue dans Transformers avec le formalisme des grammaires attribuées. Le travail effectué présentera une comparaison entre ce formalisme et deux autres techniques de désambiguisation : la première à l'aide d'ASF+SDF et la deuxième à l'aide du langage Stratego. Le but de cette comparaison sera double : montrer que les grammaires attribuées sont parfaitement adaptées à ce problème et exhiber les faiblesses de celles-ci par rapport aux deux autres méthodes en vue d'une amélioration possible du système utilisé dans Transformers. +
Modularity, scalability and expressiveness, three main aspects for a disambiguation system. Disambiguation is the step occurring just after the parsing that consists in analyzing the output given by a generalized LR parser. The goal is to choose, amongst the many parse trees, the right one that corresponds to the input using semantics rules. By means of a comparison with two other methods based on SDF (the first one using ASF formalism and the second one using Stratego language), our approach, attribute grammars, will be evaluated with respect to these three aspects to bring out its strengths and its weaknesses. +
Modularité, extensibilité et expressivité, trois aspects fondamentaux pour un système de désambiguïsation. La désambiguïsation est l'étape survenant juste après l'analyse syntaxique qui consiste à analyser la sortie obtenue lors de l'utilisation d'un parseur LR généralisé. Le but de cette étape étant de sélectionner, parmi toute une forêtl'unique arbre valide correspondant à l'entrée en prenant en compte les règles de sémantique contextuelles. Au travers d'une comparaison avec deux autres techniques reposant sur SDF (le formalisme ASF et le langage Stratego), le système de grammaires attribuées utilisé dans Transformers sera évalu par rapport à ces aspect fondamentaux pour en faire ressortir les avantages et inconvénients. +
The Automata-Theoretic approach to model checking traditionally relies on Büchi Automata (BA) which we want as small as possible. Spot, a model-checking library, uses mainly TGBA: a BA generalization. We have already presented a simulation reduction (called direct) that works on TGBA. This algorithm is included in Spot 0.9 and led to produce smaller automata than in the previous versions of Spot. The simulation consists in merging states that recognize the same infinite suffixes. We show that we can also work on infinite prefixes (it is called cosimulation), and that we can iterate these two simulations to create the iterated simulation. This iteration-based simulation, included in Spot 1.0, is a clear improvement over our previous simulation procedure. We finally experiment a method that consists in considering some acceptance conditions as don't care. Since the acceptance conditions on transitions that are not on a Strongly Connected Component have no influence on the language, we can change them to help the simulations. +
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 2019 BraTS Challenge. We want to improve the segmentation results submitted last year by LRDE's team, using a 2-step 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. Improvements are done through robustness assessment, study of image features, and new method. +
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 2019 BraTS Challenge. We want to improve the segmentation results submitted last year by LRDE's team, using a 2-step 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. Improvements are done through new method, modification of networks, and assement of calibration +
Software engineering defines some methods in order to guarantee software quality. In the image processing fieldseveral image types exist. Also, this is difficult to build a library dedicated to this field which provides reusableextensible or compatible tools. We will see different approaches used by generic image processing libraries which deal with this problem. +
Software engineering defines some methods in order to guarantee software quality. In the image processing fieldseveral image types exist. Also, this is difficult to build a library dedicated to this field which provides reusableextensible or compatible tools. We will see different approaches used by generic image processing libraries which deal with this problem. +
La séparation de locuteur et la détection de voix jouent un important rôle dans les systèmes de reconnaissance du locuteur, principalement dans le cas d'un signal à plusieurs locuteurs.Nous allons présenter une méthode de séparation de locuteur basée sur des méthodes variationnelles et sur les speaker factors tel que décrite dans l'état de l'art de systèmes de reconnaissance du locuteur. Afin de tester les performances de cette méthode un ensemble de tests sera effectué sur les données interview de NIST-SRE 2010. +
During the last years, sound source separation has been a subject of intense research. In meetings or noisy public places, often a number of speakers are active simultaneously and the sources of interest need to be separated from interfering speech in order to be robustly recognized. An effective algorithm is the Independent Component Analysis (ICA). ICA models the mixture signal as a standard form of linear superposition of source signals. Under difficult environmental conditions, ICA outputs may still contain strong residual components of the interfering speakers. We will use this algorithm for speaker diarization in verification system. We will obtain better results especially in the case of multi-speaker audio datasuch as interview or microphone segment of NIST Speaker Recognition Evaluation. +
Speaker diarization has emerged as an increasingly important and dedicated domain of speech research. It relates to the problem of determining "who spoke when ?". It means that we would like to find the intervals during which eachspeaker is active. By computing the Mel Frequency Cepstral Coefficients (MFCC) features from a given speech signal and using the Independent Component Analysis (ICA) on these features, we are able to segment the speech, with the help of a Hidden Markov Model (HMM). We will use this algorithm for speaker diarization in verification systemwith multi-speaker audio data, such as interview of microphone segment of NIST Speaker Recognition Evaluation. +
The i-vector is actually the state of the art in speaker verification. Efficient result was achieved using classifier such as Cosine Distance (CD). Howeverclassification is performed on a global channel compensated i-vector. In this study, we explore the possibility to enroll a speaker and define a speaker specific channel compensation using i-vector. The objective is to improve the classifier performance using our previous work on Self-Organizing Map to select suitable i-vector. We will compare the performance of our solution with the global channel compensated method. +
To represent a system by an automaton, we have to save the values of all variables of this system in each state. This can take a lot of memory when there is a lot of variables and/or a lot of states, and also can grow the execution time due to cache misses. To avoid this problem in Spot, we compress the array of variables of each state, which already reduces the memory consumption and the execution time. In this report, we present a datastructure for a better compression of variables in states, using the redundancy of the values in each states of the automatonand the different constraints encounter to add it in Spot. +
Emptiness-checks enable to know if the language of an automaton is empty or not. These checks are often used in model checking: unfortunately, they are very expensiveparticularly if the automaton is neither weak nor terminal. In order to reduce this expensive check, this work implements an option that permits the extraction of three smaller automata capturing the terminal, weak, and remaining strong components from the original automaton, so that the three corresponding emptiness checks can be performed independently using the most appropriate algorithm. +
The Transformers project aims at providing source to source transformations for C and C++ languages. This consists in parsing the input source, a C/C++ source code extended to accept new syntactic rules. The input code is then transformed into standard C/C++. This is similar to the process used by the C++ ancestor, “C with classes”which was an extension of C and which was transformed into C before being compiled. We will show how to write an extension of the C++ grammar using the Transformers project, and to transform the extended C++ input into standard C++. For this purpose, we will use extensions that have already been implemented (ContractC++class-namespaces) as examples. We will analyse to what extent the technologies like attribute grammars used in Transformers help us. +
The discrimination of characters is an important domain of optical characters recognition. The goal is to determine if a delimited surface of an image is a character or not, with rotation invariance. We are able to reduce the redundant information by doing a principal component analysis (PCA) on the training data set. Then, we use the probabilistic linear discriminant analysis (PLDA) algorithm to models both intra-class and inter-class variance as mutli-dimensional Gaussians. The performance of the new model will be compared with the one currently used in the optical characters recognition application of Olena. +
Ce rapport expose des fac c ons performantes et génériques d'implémenter la suppression de transitions spontanées dans un varepsilon-NFA. Nous comparons deux approches : l'algorithme d'varepsilon-clôture de J. Sakarovitch et S. Lombardyet l'algorithme d'varepsilon-suppression de M. Mohri. Nous discutons de la fac c on dont ces algorithmes peuvent être implémentés dans le cas d'automates pondérés génériques, ainsi que de leur performance, en comparant des résultats empiriques obtenus dans Vcsn. +
Lors de cette présentation, un algorithme de resynchronisation sera décrit ainsi que son implémentation dans Vaucanson. De plus, des explications sont données sur l'ajout des transducteurs a délai borné, ainsi que sur les difficultés qui peuvent être rencontrées lors de l'extension de la hierarchie de classes de Vaucanson. +
Synchronous rational relations is the largest subfamily of rational relations so far defined that is an effective Boolean algebra. It can be therefore of some interest to provide manipulation tools which might help in their study. With the recently added support of pair-alphabets in Vaucanson, we suggest a new approach to deal with synchronous rational relations represented as letter-to-letter transducers and provide the necessary tools to work with them. +
Nous présentons un nouvel outil de synthèse de circuit à partir de spécifications LTL. Il réduit le problème de synthèse à un jeu à parité en exploitant la bibliothèque Spot pour manipuler efficacement les ω-automates. Deux méthodes ont été implémentées pour la résolution du jeu: l'algorithme récemment découvert par Calude et al., qui a la meilleure compléxité théorique connue pour ce problème, et l'algorithme récursif de Zielonka, connu pour ses bonnes performances pratique. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d'origine. +
Dans la reconnaissance du locuteur, les modèles GMM occupent une place très importante dans le développement des systèmes performants. Les méthodes de discrimination linéaire à base de SVM donnent actuellement de meilleurs résultats. On s'intéressera ici à un système de discriminant linéaire (le SVM-GLDS). Celui-ci utilise directement, sans passer par un modèle GMM, des statistiques issues de l'ensemble des paramètres de la parole pour définir le modèle de reconnaissance. On évaluera les performances d'un tel système sur la base de données NIST-SRE en le comparant avec les autres systèmes à base de SVM-GMM. +
La séparation de locuteur et la détection de voix jouent un important rôle dans les systèmes de reconnaissance du locuteur, principalement dans le cas d'un signal à plusieurs locuteurs.Nous allons présenter une méthode de séparation de locuteur basée sur des méthodes variationnelles et sur les speaker factors tel que décrite dans l'état de l'art de systèmes de reconnaissance du locuteur. Afin de tester les performances de cette méthode un ensemble de tests sera effectué sur les données interview de NIST-SRE 2010. +
T
Tarjan Union-Find algorithm (TUFA) aims to build, given an image, a tree representation modeling the equivalence classes following a given relation. It can be derived to define filters on those tree representations. TUFA is currently used in Milena, our image processing library, to implement connected filters. For example, closing and opening related to area, volume, or height which are useful to clean an image while preserving contours. This important property provides a nice advantage in comparison to the classical opening and closing based on erosion and dilation. Another advantage of TUFA is that it can be used for algorithms which feature the domain disjointness property. This document presents how new connected filtersin particular self-dual, have been introduced into Milena. +
Milena est la bibliothèque de traitement d'image générique de la plate-forme Olena. Cette bibliothèque a pour but d'être performante tout en restant simple. L'introduction dans Milena de nouveaux types d'images basés sur des graphes a mis en évidence des problèmes de modélisation qui sont un frein pour sa généricité. Par exemple, nous avons toujours considéré que "les images ont des points". Néanmoinscertains types d'images possèdent des sites qui ne sont pas des points (mais des arrêtes, faces, ou même des ensembles de points). Une autre supposition erronée était de considérer que les sites étaient toujours localisés par un vecteur (càd, (x,y) dans le plan 2D). Cette supposition est fausse lorsque l'on manipule des sites qui ne sont pas "Pointwise". Il etait donc nécessaire de modifier les types d'images utilisés dans Milena et les propriétés qui leur sont associées. Pendant ce séminaire, nous présenterons une nouvelle classification d'images permettant de résoudre ces problèmes. +
Spot est une bibliothèque qui manipule des ω-automates dont les conditions d'acceptation sont exprimées avec au plus 32 ensembles d'acceptation. Puisque la condition d'acceptation du produit de deux automates doit utiliser la somme de leurs ensembles, on ne peut pas construire des produits dont les opérandes utilisent plus de 32 ensembles au total. Une opération typique sur les automates est de calculer L(Atimes B)neemptyset pour décider si L(A) intersecte L(B). Lorsqu'elle est implémentée par empty(product(A, B))le calcul du produit limite le nombre d'ensembles d'acceptation que A et B peuvent utiliser. On propose une nouvelle fonction empty(A, B) qui réalise le test de vacuité de Atimes B sans construire un automate et donc sans limite sur les conditions d'acceptation. L'outil ltlcross peut maintenant comparer des automates pour un total supérieur á 32 ensembles d'acceptation. +
Il existe une hiérarchie de propriétés temporellesdéfinie par Manna et Pnueli (1990). Cette hiérarchie contient entre autres les classes de récurrence et persistence. Savoir si une formule de logique temporelle à temps linéaire (LTL) f est récurrente (respectivement persistente) est intéressant car cela guarantit que f peut être traduit en un automate de Büchi déterministe (respectivement en un automate de co-Büchi). Auparavant, Spot, une bibliothèque de manipulation de formules LTL avait une unique façon de tester l'appartenance d'une formule aux classes de persistence ou récurrence. Grâce à nos précédents travaux présentés dans emphA co-Büching Toolbox +
Here is a method to differentiate text from non-text inside a picture using descriptors inspired by data compression algorithms. The major goal of this approch is to compute a signal that will allow a learning system (like knn or svn) to classify text and background of an image. To compute this signal a wavelet based method, similar to the one used in png or jpeg compression format, will be used. Another point that will be discussed is what kind of wavelet gives the best results and with what kind of learning system.These descriptors will then be compared whith other descriptors that are not wavelet based. Finaly the various way to reduce the time spent to compute the descriptors will be presented like the wavelet lifting. +
The Tree of Shapes is an useful image transform used to process digital images in a self-dual way. It can be computed using several approaches available on the literature though no comparison of those algorithms exists yet. We provide a comparison of the existing algorithms from the computation time and space occupation point of view. We also study further the quasi-linear algorithm based on the union-find providing a parallel version and use a slight modification of the intermediate representation of images it manipulates to improve both its practical computation times and space requirements. +
In speaker recognition, deep neural networks (DNN) have recently proved to be more efficient than traditional gaussian mixture models (GMM) for collecting Baum-Welch statistics that can be used for i-vector extraction. However, this type of architecture can be too slow at evaluation time, requiring a GPU to achieve real-time performance. We show how triphone posteriors produced by a time delay neural network (TDNN) can be used to create a more lightweight supervised GMM serving as a universal background model (UBM) inside the i-vector framework. The equal error rate (EER) obtained with this approach is compared to those obtained with traditional GMM-based UBM. +
Dividing a picture into area of interest is called picture segmentation, it is useful in particular to point out cancerous cells in medical imaging. The emphWatershed Transform provides such a segementation and can be implemented in many ways. Here we will focus on the emph Topological Watershed, a performant algorithm producing results with nice properties. In this report, we will show how this algorithm had been implemented in Milena, the C++ generic image processing library of Olena, developed at the LRDE. We will first see how to treat usual image format and then generalize it to trickier formats like pictures mapped on general graphs. +
Vaucanson is a finite state machine manipulation platform for automata and transducers. Usage highlighted the overly complex interface for the automaton manipulation. Therefore, a new approach to its definition was considered involving the concept of automaton kinds. The former Vaucanson development team initiated this series of fundamental changes which concluded in the implementation of the labels-are-letters kind. Still, these changes put the library in a transitional state. newline In the continuation of their work and in order to restore both the robustness and genericity of Vaucanson, we will introduce two new kinds into the library: labels-are-words and labels-are-series. This work may lead to a series of changes involving both algorithm rewriting and data structure modifications which will allow simpler yet more powerful automata manipulation. +
Vaucanson is a finite-state machine manipulation platform for automata and transducers. Usage and development highlight complexity and ineffectual. Active work on specifications and design have been undertaken to introduce, in the core of Vaucanson, easier mechanism to the library manipulation and development. The version 2.0 is, today in development. This report presents the 2.0 version of Vaucanson and his usability with the portage of two algorithms: Evaluation of word in automata and determinization of automata. Next, we show the new design profit compared to Vaucanson 1.4 related to the speedup. +
Spot repose sur l'approche automate du emphmodel checking. La bibliothèque permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur une modélisation d'un système représentée par un automate de Büchi généralisé basé sur les transitions (TGBA). Spot propose actuellement deux algorithmes de traduction de LTL en TGBAune des deux étapes principales de l'approche automate. Nous présentons une nouvelle traduction en TGBA d'une logique LTL qui a été étendue en y ajoutant des opérateurs représentés par des automates finis. Cette traduction permet à Spot de vérifier des propriétés qui n'étaient pas exprimables auparavant. +
Spot est une bibliothèque de model checking qui permet de vérifier des propriétés exprimées en logique temporelle à temps linéaire (LTL) sur des modèles représentés par des automates de Büchi généralisés basés sur les transitions (TGBA). Spot propose actuellement deux algorithmes de traduction de LTL en TGBA, une des étapes principales de l'approche automate. Nous présentons une nouvelle traduction en TGBA d'une LTL étendue dont les opérateurs sont représentés par des automates finis, permettant ainsi à Spot de vérifier des propriétés qui n'étaient pas exprimables auparavant. Nous présenterons aussi de quelles fac cons nous pourrions intégrer certaines fonctionnalités de PSL (Property Specification Language) à notre extension. +
En vérification formelle de la logique temporelle linéaire (LTL) à l'aide d'ω-automates, la négation d'une formule LTL est traduite en ω-automate. La construction d'un automate plus petit réduit beaucoup le temps d'exécution et la consommation mémoire des opérations suivantes de la chaîne de traitement de la vérification formelle. Müller et Sickert ont présenté une méthode efficace pour traduire n'importe quelle formule LTL en un petit automate déterministe. Cette méthode consiste à découper la formule en trois ensembles de sous-formules qui appartiennent respectivement au fragment de sureté ou de garantie, au fragment d'équité et au reste. Ils traduisent ensuite individuellement ces ensembles de sous-formules en automates déterministes qu'ils combinent par la suite. Spot peut déjà traduire les formules d'obligation en automates déterministes minimaux. Les formules d'obligation étant un surensemble des formules de sureté et de garantie, on généralise la traduction de Müller et Sickert en remplaçant le fragment de sureté ou de garantie par le fragment d'obligation. En ce qui concerne le fragment d'équité, ils ont présenté un algorithme de traduction efficace qui produit de petits automates déterministes. Ils ont également présenté comment construire efficacement un produit de ces automates avec d'autres automates. Nous présentons comment nous implémentons ces deux méthodes dans Spot. +
Vaucanson permet de manipuler des automates finis. La modélisation de ces objets occupe donc une place centrale dans 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. Nous exposerons ce qui peut être considéré comme un véritable nud gordien dans la modélisation actuelle: Vaucanson est par exemple incapable de choisir une implémentation pour un automate en fonction d'une de ses propriétés. La solution apportée restaure alors une modélisation saine et empêchera des erreurs de conception lors de la recherche de spécifications des algorithmes. Finalementnous exposerons, entre autre, une série de spécialisations du concept d'automate, ainsi qu'un ensemble d'améliorations du modèle qui étaient autrefois trop coûteuses à mettre en place. +
L'application de filtres morphologiques sur une image en niveaux de gris permet d'en faire disparaître certaines parties et d'en mettre en valeur d'autres. De ce fait, en choisissant un élément structurant adapté, il est possible d'éliminer certains éléments d'une carte comme le texte et de reformer les lignes discontinues. Un banc de filtres a été défini permettant de récupérer les lignes fines de l'image, frontières des parcelles, et ce, quelle que soit leur orientation. Sur l'image résultante, un algorithme de partage des eaux peut mettre en évidence les parcelles recherchées. Par ailleurs, l'application d'un algorithme de seam carving permet de retirer, en pré-traitement, d'éventuelles lignes de quadrillage. +
Transducers are used in many fields, such as linguistics to model phonological rules, regular expressionsspecification languages, speech recognition... When working with transducers, one of the most indispensable tools is composition. As such, it is essential to implement it in Vaucanson 2 in an efficient way. This report will introduce the ground work to bring about transducers composition, and then its implementation and optimization. The composition is viewed here as a special case of the product of automata with spontaneous transitions, so three algorithms for this product are exposed here, as well as some essential implementation concepts. +
Vaucanson is a library dedicated to finite automaton manipulation devlopped by the Research and Development Laboratory of EPITA (LRDE). This project aims at providing its users with a great variety of automaton typesincluding transducers. This report suggests an implementation of generic transucers, which accept automaton labeled by tuples of languages. +
Vaucanson est une bibliothèque dédiée à la manipulation d'automates finis développée par le Laboratoire de Recherche et Developpement de l'EPITA (LRDE). Ce projet tient à offrir à ses utilisateurs une large variété de types d'automates, notamment les transducteurs. Ce rapport propose une implémentation de transducteurs génériques, qui peuvent accepter des automates étiquetés par des n-uplets de langages. +
Lors de cette présentation, un algorithme de resynchronisation sera décrit ainsi que son implémentation dans Vaucanson. De plus, des explications sont données sur l'ajout des transducteurs a délai borné, ainsi que sur les difficultés qui peuvent être rencontrées lors de l'extension de la hierarchie de classes de Vaucanson. +
FIXME +
Dans ce rapport technique, nous nous attardons sur le jeu de la tablette de chocolat. On dispose d'une tablette de chocolat dont le carré inférieur gauche est empoisonné. Les joueurs jouent à tour de rôle. Un coup consiste à choisir un carré de chocolat et à le manger ainsi que tous les carrés qui sont à sa droite et au dessus de lui. Le joueur qui mange le carré empoisonné perd la partie. Dans cet exposé, nous nous intéresserons particulièrement au cas où les dimensions du jeu sont de classe cardinale infinie. On présentera également, pour une meilleure compréhension, les nombres ordinaux et leur ordre associé. +
La transformation rapide des courbes de niveaux (FLLT) construit une représentation d'une image indépendante du contraste. Cet algorithme construit un arbre suivant les inclusions des formes. Pour un filtre, être invariant suivant le contraste est un plus. Par exemple, en analyse de document, cette représentation a le précieux avantage d'extraire facilement et rapidement les caractères indépendamment du fait qu'ils soient plus clairs ou plus foncés que leur voisinage. Ce document présente l'introduction de l'algorithme dans notre bibliothèque de traitement d'images et montre les résultats de quelques filtres connectés que peut engendrer cette représentation. +
Le but du projet Transformers est de créer un ensemble d'outils de manipulation de C et C++. Une fois achevé, il simplifiera la création d'outils de transformation ou d'analyse pour le C++. Il permettra aussi d'expérimenter des extensions du langage. Les étudiants du groupe Transformers ont travaillé pendant des annéespassant chaque année le résultat de leur travail à la génération suivante. De nombreux outils ont été créés, chacun d'eux résolvant (ou tentant de résoudre) un problème auquel nous sommes confrontés en essayant de manipuler du C++. Des dizaines de rapports ont été écrits : certains sont obsolètes, mais d'autres sont des ressources précieuses. Il est maintenant temps de prendre du recul, de regarder le travail accompli et ce qui ne fonctionne pas encore, afin de décider si et comment nous voulons poursuivre ce projet. +
The goal of the Transformers project is to create a C and C++ manipulation framework. Once achieved, it will simplify the creation of transformation or analysis tools for the C++ language. It will also allow experiments with language extensions. Transformers' students have been working for years on the project, handing over, each yearthe results of their work to the next generation. Lots of tools have been created, each of them solving (or attempting to) a problem that we face when trying to manipulate C++ code. Tens of reports have been written. Some are outdated, but some of them are still a valuable resource. It's now time to take a step back and to have a look at what has been accomplished and what does not work yet in order to decide if and how we want to go forward on this project. +
Spot is centered around the automata approach to model checking. The library can be used to verify that every behavior of a model, a transition-based generalized Büchi automata (TGBA), satisfies a given property, expressed using an linear temporal logic (LTL) formula. Spot offers two translation algorithms of LTL into TGBA, one of the two main stages of the approach. We present a new translation into TGBA of a LTL logic which has been extended by adding operators represented by finite automaton. This translation allows Spot to verify properties that were not expressible before. +
Spot is a model checking library centered around the automata approach, which 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 two translation algorithms from LTL formulæ into TGBA, one of the main stages of the approach. We present an extension of one of these algorithms to an extended LTL where operators are represented by finite automata, allowing Spot to verify properties that were not expressible before. We also present how we could integrate some features of PSL (Property Specification Language) in our extension. +
In a previous paper we introduced the two-automaton emptiness check in the Spot library, that would check for the emptiness of the intersection of the languages of two '"`UNIQ--math-00000003-QINU`"'-automata without building their productcircumventing a limitation in Spot on the number of acceptance sets of the automata. This operation, when the intersection is actually not empty, is usually followed by an accepting run search on the product that would return an example of such a word that is in the languages of both automata. We introduce a new method that computes an accepting run from the data gathered during the two-automaton emptiness check, allowing us to use this new method in algorithms that require the counterexample. +
Spot is library that handles '"`UNIQ--math-00000009-QINU`"'-automata whose acceptance conditions are expressed with at most 32 acceptance sets. Since the acceptance condition of the product of two automata has to use the sum of their setswe cannot produce a product whose operands use more than 32 sets in total. A typical operation on automata is to compute '"`UNIQ--math-0000000A-QINU`"' to know if '"`UNIQ--math-0000000B-QINU`"' intersects '"`UNIQ--math-0000000C-QINU`"'. When it is implemented as '"`UNIQ--math-0000000D-QINU`"', the computation of the product throttles the amout of acceptance sets A and B can use. We propose a new function '"`UNIQ--math-0000000E-QINU`"' which does the emptiness check of '"`UNIQ--math-0000000F-QINU`"' without actually building an automaton and hence without any limit on the acceptance conditions. The ltlcross tool can now compare automata using a total of more than 32 acceptance sets. +
U
Spot est une bibliothèque extensible pour le model checking qui utilise les automates de Büchi généralisés à transitions acceptantes. Il contient de nombreux algorithmes de pointes. Dans ce papier, on se concentre sur deux de ses algorithmes qui construisent des automates avec plus de transitions que nécessaire. En pratique ces constructions utiliseraient moins de transitions si elles pouvaient calculer un feedback arc set (FAS), c'est-à-dire un ensemble de transitions à retirer du graphe pour le rendre acyclique. Dans l'absoluon veut un FAS minimal, mais ce problème est NP-difficile. On adapte et améliore une heuristique proposée par Eades et al. qui permet une construction en temps linéaire. On montre comment cet algorithme bénéficie à la complémentation d'automates de Büchi déterministes et la traduction d'automates de Rabin en automates de Büchi. En fonction de l'automata traité on remarque une amélioration montant jusqu'à 31%. Ces résultats varient beaucoup selon le nombre de cycles et d'états acceptant. +
Ces dernières années, les opérateurs connectés ont gagné une certaine popularité dans le domaine du traitement d'images, ils ont en effet été largement utilisés dans le cadre de filtrage, de segmentation, de détection d'objets...Néanmoins, plusieurs défauts ont été mis en évidence, le plus important étant la dépendance au contraste, on ne peut que détecter soit les objets clairs, soit les objets foncés. Les opérateurs auto-duaux permettent d'opérer sur les objets clairs et foncés à la fois et ne souffrent donc pas du défaut des opérateurs connectés classiques. En revanche, les opérateurs auto-duaux sont plus difficiles à mettre en place et les algorithmes actuellement disponibles sont coûteux en temps de calcul. Nous proposons un nouvel algorithme pour calculer les opérateurs auto-duaux basés sur l'union-find de Tarjan; celui-ci offrant de meilleures performances que l'algorithme d'arbre de contours à l'état de l'art. +
Grâce au format HOA, il y a de moins en moins de barrières entre des ω-automates avec différentes conditions d'acceptation. Spot, une bibliothèque manipulant les ω-automates supporte des conditions d'acceptations arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversions capables de convertir (quand c'est possible) n'importe quelle condition d'acceptation classique vers du co-Büchi déterministe. Boker and Kupferman ont mis au point des méthodes asymptotiquement optimales réalisant ces conversions. Nous avons implémenté leurs méthodes avec quelques optimisations et adaptations: nous supportons les conditions d'acceptations dites "Streett-like", celles écrites sous forme normale disjonctive (y compris celles dites "Rabin-like") ainsi que les acceptations basées sur les transitions ("transition-based"). Ces algorithmes peuvent être utilisés pour vérifier si une formule LTL est de la famille "persistence". +
Une implementation efficace de déterminisation d'automates de Büchi généralisés à transitions acceptantes +
Dans le model checking probabiliste, l'utilisation d' ω-automates déterministes permet de faciliter les calculs probabilistes grâce à l'unicité de chaque chemin. Malheureusement, il existe peu de traducteurs LTL qui produisent des ω-automates déterministes. De plus, ceux produits par Spot, une bibliothèques de model checking, ne le sont pas forcément. La powerset construction n'arrive pas toujours à déterminiser les automates de Büchi. Cependant, en mémorisant les chemins acceptants, la construction de Safra arrive à convertir les automates nondéterministes de Büchi en automates déterministes de Rabin. Le changement de condition d'acceptation est nécessaire car les automates de Büchi déterministes sont moins expressifs que leurs variantes nondéterministes. L'implémentation de cette construction permettra à Spot de déterminiser tous types d'automates et de calculer leurs compléments. Dans ce papier, on verra comment implémenter de manière efficace cette construction et comment l'étendre à la déterminisation d'automates de Büchi généralisés à transitions acceptantes. +
SCOOL est un langage dédié (DSL) destiné à faciliter le développement C++ de haut-niveau. Fondé sur le paradigme SCOOP mélangeant programmation générique et orientée-objet, il se démarque par une résolution statique des appels de fonctions membres et un système de concepts puissant. Précédemment, une bibliothèque de conteneurs standards a été réalisée en C++ grâce à SCOOP. Cette implémentation demandait cependant une forte maîtrise des mécanismes de SCOOP. Avec SCOOL, nous pouvons y arriver sans se préoccuper des détails, laissés au traducteur C++. En se concentrant sur le développement de la bibliothèque en SCOOL et sur les changements nécessaires au langage et à son compilateur, nous comparerons les solutions originales et à base de DSL et déterminerons si SCOOL est adapté au prototypage d'applications génériques. +
Cxx a réussi à supporter à la fois la programmation orienté objet classique et la programmation générique, cependant certains problèmes récurrents restent toujours difficiles à résoudre. Scoop est un paradigme orienté objet. Il fournit des méthodes virtuelles, les arguments covariants, les types virtuels et les multi-méthodes typées statiquement sans avoir besoin d'étendre le langage. Scoop utilise sa propre bibliothèque Cxx pour facilier la conception d'une bibliothèque utilisant ce paradigme. +
The text-localization system developed by the laboratory currently uses a wavelet-based descriptor to separate text from background in natural images. Benchmarks show that this descriptor is fast and accurate when performing this task. Our main objective is to extract shape information when performing classification using the same descriptor as the one used to separate text from background. Such data is useful improving the accuracy of other steps in the text localization system. Moreover, because the descriptor used to extract shape information has already been computedthis approach is not CPU consumin. More than shape information, the wavelet based descriptor can be extended again to create a simple O.C.R. (Optical Character Recognition). However in order to extract this data without changing the structure of the descriptor, some changes must be done in the classification process and in the learning process. Various methods to achieve these goals are presented and compared in order to see what kind of information could be extracted with the wavelet-based descriptor. +
Connected operators are morphological filters which have the property of keeping objects contours when simplifying images. They bring to the light objects situated in the image. To do it, an implementation of the Tarjan's Union-find algorithm is used for an easy manipulation of image components. A binary partition tree is built, in order to simplify the objects attributes computation and the filtering of image. First of all, we will introduce morphological filters and connected operators, then we will propose an overview of different kinds of methods used in the literature in order to create a binary partition tree and we will explain the Tarjan's "union-find" algorithm for the image filtering. At last, we will apply this method in order to clean and delete stars in space's images. +
Connected operators are morphological filters which have the property of keeping objects contours when simplifying images. They bring to the light objects situated in the image. To do it, an implementation of the Tarjan's Union-find algorithm is used for an easy manipulation of image components. A binary partition tree is built, in order to simplify the objects attributes computation and the filtering of image. First of all, we will introduce morphological filters and connected operators, then we will propose an overview of different kinds of methods used in the literature in order to create a binary partition tree and we will explain the Tarjan's "union-find" algorithm for the image filtering. At last, we will apply this method in order to clean and delete stars in space's images. +
We will propose a method that has the objective of improving text detection in natural images. First of allwe will present the Mumford-Shah segmentation methodbefore explaining how to integrate this method into the laboratory's current toolchain (TextCatcher). Finally, we will evaluate the new text localisation error rate given by this segmentation. +
Utilisation d'un descripteur à base de transformée en ondelettes pour extraire des informations sur la forme des objets +
Le système de localisation de texte développé par le laboratoire est actuellement en mesure de séparer le texte du fond dans les images naturelles au moyen d'un descripteur basé sur la transformée en ondelettes. De plus, les tests montrent que ce système est rapide et précis pour accomplir cette tâche. Notre objectif principal est d'extraire de nouvelles informations sur la forme des objets lors de la phase de classification en utilisant le même descriteur que celui utilisé pour séparer le texte du fond. De telles informations peuvent être utilisées pour améliorer la précision d'autres étapes du système de localisation de texte. De pluspuisque le descripteur utilisé pour extraire ces informations à déjà été calculé, cette approche est peu consommatrice en temps CPU. Par ailleurs, plus que des informations sur la forme des objets, ce descripteur peut également être utilisé tel quel pour créer un O.C.R. (Reconnaissance optique de caractère) simple. Cependant, afin de mettre en place ces changements, il est nécessaire de retravailler le système de classification et le système d'apprentissage mis en place précédemment. Différentes méthodes pour atteindre ces objectifs sont présentées ici et comparées afin de savoir quelle sorte d'information il est possible d'extraire à partir du descripteur à base de transformé en ondelettes. +
Nous proposerons une méthode pour améliorer la détection de texte dans des images naturelles. Nous présenterons d'abord la méthode de segmentation de Mumford-Shah, puis nous examinerons comment l'intégrer dans le pipeline de détection de texte du laboratoire (TextCatcher). Enfin, nous évaluerons les nouveaux résultats de localisation de texte obtenues avec cette ségmentation. +
V
Image inpainting is the process of reconstructing parts of an image in a visually plausible way. A category of methods well established in the literature is based on partial differential equations (PDE). The PDE approach consists in iteratively propagating geometric and intensity information into the missing area. However designing such models requires deep insights and mathematical understanding of the problem at hand. Based on Risheng Liu's paper for building the PDE in a bottom up manner using linear combinations of invariants, we propose an optimized implementation that we compare to previous methods. +
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 kinds. newline The library interface was remade, and so were its internal mechanics. This led to a series of changes in data structures, algorithms and interface definition. We will expose these modifications while trying to highlight the various pitfalls one may encounter when working directly in the library core. This work may lead to a performance analysis between Vaucanson 2.0 and the last stable release of the library. +
Linguistics is one of the field of application of the automata theory, the latter being used to represent and manipulate languages. Vcsn has yet to be used for such applications. With the recent implementation of efficient composition, it was made possible to use the library to create a translator using transducers. This work will present the different steps of implementation of a translator from text language ("bjr") to french ("bonjour") using Vcsn, and the pipeline of the translating process using automata. We will go through the difficulties encountered during this implementation, from the absence of some algorithms to the poor performances of others. +
La théorie des automates étant utilisée pour représenter et manipuler des langages, la linguistique en est un des domaines d'application. La bibliothèque Vcsn n'a pas encore été utilisée pour de telles applications. La récente implémentation d'une méthode efficace de composition a rendu possible la création d'un traducteur utilisant des transducteurs. Nous présenterons les différentes étapes de l'implémentation d'un traducteur de language SMS ("bjr") vers le français ("bonjour") en utilisant Vcsn, et le pipeline du processus de traduction utilisant des automates. Nous verrons également les difficultés qu'a amenées son implémentation: de l'absence de certains algorithmes dans Vcsn aux mauvaises performances d'autres. +
Verification de proprietes sur un programme en utilisant de l'analyse statique et de la verification de modele +
Dans ce papier, nous presentons les differentes solutions pour transformer un programme en un systeme d'etats finis. Puis nous presentons notre programme fonctionnel qui nous permet de dire si un programme en C verifie ou non une formule LTL. Nous decrivons tous les aspect de ce programme, que ce soit de l'utilisation de LLVM, d'un algorithme C++ d'abstraction de modeles ou encore de la bibliotheque Spot. Dans une premiere partie, nous expliquons quel type de graphe fini nous voulons obtenir comme modele du programme. Dans une deuxieme partie, nous definissons des notions importantes de la verification de modeles, tels que les systemes de poussee ou les automates de Buchi. Dans une troisieme partie, nous expliquons comment trouver une sous-approximation et sur-approximation d'un systeme de poussee vers un systeme d'etats finis. Pour finir, nous montrons comment ces solutions theoriques sont implementees en un vrai programme fonctionnel +
In this paper, we present different solutions to transform a program into a finite state system. Then we present our functional pipeline that allows us the say whether a program verifies a LTL formula. We describe all the aspect of this pipeline from LLVM tools and a C++ algorithm for model abstraction to the Spot library. On a first part of this paper, we explain the type of finite graph that we want to obtain in order to apply model checking in. On a second part, we define important models such as pushdown systems or Buchi automaton. On a third part, we explain how to find an under-approximation and over-approximation of a pushdown system as a finite system. Then finally, we show how those theoretical solutions were implemented into an actual functional pipeline. +
Vaucanson est une plateforme de manipulation d'automates finis et de transducteurs dont l'interface s'est montrée trop complexe. Une nouvelle approche de sa définition fut par conséquent considérée, impliquant l'utilisation du concept de kind d'un automate. La précédente équipe de développement de Vaucanson implémenta le kind labels-are-letters, ce qui laissa la bibliothéque dans un état transitoire. Afin de restaurer la force et la généricité de Vaucanson, le nouveau kind labels-are-words sera introduit. Ce travail ménera à plusieurs changements, de la réécriture d'algorithmes à la modification du design de la bibliothéque. +
Vaucanson est une plate-forme de manipulation d'automates et de transducteurs dont l'interface et le développement se sont montrés complexes et inefficaces. Des travaux de spécifications et de design ont été effectués afin d'avoir un coeur efficace en terme de développement et de vitesse. Cette version 2.0 de Vaucanson est actuellement en développement. Ce rapport présente la version 2.0 de Vaucanson et son utilisation par le portage de deux algorithmes : l'évaluation d'un mot par un automate et la déterminisation d'automates. Dans une seconde partienous montrerons si Vaucanson 2.0 tient ses promesses en termes de vitesse d'exécution. +
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. +
W
Climb is a generic image processing library written in Lisp. The study of the implementation of a segmentation algorithm by computing watersheds highlights the possibilities offered by the combination of a dynamic language like Lisp and a generic image representation. This case study tackles basic concepts of manipulating images in Climb like: sites, site-sets and accumulators. +
X
The XML Proposal presented at CIAA 2005 (Conference on Implementation and Application of Automata) and updated by Florent Teronnes has some lacks. For example, labels with regular expressions were not clearly defined. Our work has for objective to finalize the proposal of a universal description format for automata to make communication between various tools easier. The second part of our work is to update Vaucanson to support this new format, with a reimplementation of its XML parser. It allowed us to change our parser from a DOM model to a SAX one, reducing memory usage and improving Vaucanson's input performances. +
La proposition XML présentée à CIAA 2005 (Conference on Implementation and Application of Automata) et enrichie depuis par Florent Terrones montrait certaines lacunes. Par exemple, la gestion des expressions rationnelles n'y était pas clairement définie. Ce travail avait pour but de finaliser la proposition d'un format universel pour la description d'automates afin de faciliter la communication entre les divers outils qui leur sont consacrés et de reviser le parser de Vaucanson. +
Y
Vaucanson is a finite state machine manipulation platform. Since it was started in 2002, the project has been attracting more and more users. In that regard, it requires an efficient user front end.par For non-expert usersautomaton manipulation can be done via taf-kit, a set of command-line tools. A first GUI was developed in 2005. Its use was slow and complicated since it relied on taf-kit for every operation.par This new GUI, plugged directly into the core of the Vaucanson library for efficiencysimplifies the automaton manipulation process and makes full use of the generic algorithms included in the library. +
e
Reactive Modules is a formal model used to represent synchronous and asynchronous components of a system. PRISM is a widely used probabilistic model-checker. It introduced the PRISM language, highly based on the Reactive Modules formalism. This language quickly reaches its limit when it comes to large models. eXtended Reactive Modules (XRM) is an extension of the PRISM language. It comes with a compiler that translate XRM modules in PRISM modules, thus providing a comprehensive and reliable solution for people willing to write large models. +
Reactive Modules est un modèle formel utilisé pour décrire les éléments synchrones et asynchrones d'un système. PRISM est un outil de model-checking probabiliste. Il a introduit le langage PRISM, grandement basé sur le formalisme de Reactive Modules. Ce langage atteinte vite ses limites lorsqu'il s'agit de décrire des modèles conséquants. eXtended Reactive Modules est une extension du langage PRISM. Il est fournit avec un compilateur qui traduit les modules XRM en modules PRISMfournissant ainsi une solution fiable et complète pour les gens ayant besoin de décrire des systèmes conséquants. +
g
This technical report explores the work behind genus.py and contextualizes it within the state of the art of the genus projects. It carries on by expliciting its author's contribution, and ends by reflecting on the mistakes the author made while focusing on drawing lessons for the next generations of students. +