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