Abstract
From LRDE
M
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. +