Property

Abstract

From LRDE

Showing 20 pages using this property.
D
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.  +
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.  +