Job field
From LRDE
This is a property of type Text.
J
The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique (in Spot version 1.2) allows us to minimize deterministic Büchi automata using a SAT-solver.
To minimize a n-state deterministic Büchi automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic
Büchi automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc. +
Les méthodes d'imagerie par tomographie optique cohérente trouvent une application majeure en imagerie ophtalmique de la rétine. Mais les techniques d'imagerie confocale de l'état de l'art, basées sur l'utilisation d'une source de lumière balayée spatialement et une détection sur photodiode, sont limitées en débit (de l'ordre de 100 Mega voxel/s pour les instruments médicaux les plus aboutis actuellement). Une nouvelle gamme d'appareils de tomographie optique cohérente actuellement en cours de développement s'appuie sur des lasers accordables en longueur d'onde et une détection holographique sur caméra, permettant d'atteindre des débits de l'ordre de 10 Giga voxel/s. Leur très haute sensibilité assure un tel débit de données tout en respectant les normes médicales d'illumination de la rétine.
Les séquences recueillies sont de types "hyperspectrales": elles permettent, à un instant donné, de réaliser une cartographie des contrastes de diffusion et d'absorption optique à différents niveaux de profondeur de pénétration dans la rétine. Ces séquences, acquises à très haute fréquence temporelle, facilitent ainsi l'étude des phénomènes dynamiques tels que le flux sanguin dans les vaisseaux rétiniens.
Le volume et la cadence d'acquisition de données d'une part, et la reconstruction par calcul d'hologrammes d'autre part, jouent un rôle crucial dans la définition et l'acquisition de signaux pertinents exploitables pour l'imagerie hyperspectrale en temps réel. La visualisation en temps réel des images acquises par interférométrie holographique est en effet très gourmande en puissance de calcul, car contrairement aux méthodes de visualisation directe, des algorithmes de calcul de propagation d'ondes sont nécessaires pour reconstruire l'image à partir d'interférogrammes échantillonnés par la caméra. +
The classical theory of automata, of transducers and of rational expressions, admits a very elegant and extremely useful extension (eg, in natural language processing) taking into account the concept of weighting. The weights are then taken in a semi-ring, which can be classical (⟨𝔹, ∨, ∧⟩, ⟨ℤ, +, ×⟩, ⟨ℚ, +, ×⟩, etc..), tropical (⟨ℤ, min, +⟩, etc..), or yet of another type (e.g. rational expressions).
Vcsn is a project led by Alexandre Duret-Lutz and Akim Demaille (LRDE). It is a platform for the manipulation of automata, transducers and weighted rational expressions. It is written in C++11 avoiding the classical object-oriented programming in favor of generic programming (template) for more performance. Vcsn is an heir of the Vaucanson 2 project which was developed in partnership with Jacques Sakarovitch (Telecom ParisTech) and Sylvain Lombardy (LaBRI).
Vcsn aims at speed and user friendliness. To achieve this goal, it is built in three layers:
* ''static'': this is a templated C++ library with efficient data structures and algorithms
* ''dyn'': this C++ API support type-erasure and shields the user from the complex API of ''static'' while preserving performances. It also support code-generation and linking on the fly
* ''Python'': on top of ''dyn'', a Python binding allows a pleasant use of Vcsn, without any C++ knowledge required. +
The Spot library (https://spot.lrde.epita.fr/), written in C++11, offers several algorithms and data structures to build model checkers.
It contains many algorithms for handling linear-time temporal logic (LTL) formulas, or for different variants of Büchi automata. Spot
also distributes several command-line tools, built on top of the library. Finally, Spot includes some Python bindings, as well as a
web interface (https://spot.lrde.epita.fr/trans.html) for easy access to one of the features of the library. +
The Spot library (http://spot.lip6.fr/) contains many algorithms for translating LTL formulas into Büchi automata, and to simplify these formulas and automata. A recently added technique allows us to minimize deterministic Büchi automata using a SAT-solver; the implementation is actually not restricted to Büchi and can work with deterministic omega-automata with any acceptance conditions.
To minimize a n-state deterministic omega-automaton (an NP-complete problem) we encode its equivalence with a (n-1)-state deterministic
omega-automaton as a SAT problem, and let a SAT solver do the work of finding a solution. If such a solution is found, we try again, looking for a (n-2) state automaton, etc. +
DSL design and implementation is booming. There are many approaches to this problem, one is about using the extensibility capabilities of a general-purpose programming language in order to meet specific requirements. Many multi-paradigm approaches (eg functional languages / compile-time meta-programming) also offer benefits. Lisp is a language that is particularly well suited for this type of problem, but it is almost totally absent from the literature on DSLs. Indeed, most researchers are not (or not anymore) familiar with this language. They prefer a language based on a static approach, or have simply forgotten everything Lisp is capable of. +
R is a programming language for statistics. Because of its historical development, it has many similarities with Scheme (a language from the Lisp family), but also many problems: in particular, it is a language which is not compiled. The biggest complaint of its users is therefore its lack of performance. For this (bad) reason a number of totally esoteric features have been added to it. +
Keywords:
* image processing,
* mathematical morphology,
* tree-based reasoning,
* algorithmic optimization. +
Keywords:
* image processing,
* mathematical morphology (connected operators),
* tree of shapes,
* shaping +
Keywords:
* image processing,
* mathematical morphology,
* tree-based reasoning,
* algorithmic optimization. +
Climb est une bibliothèque de traitement d'image écrite en Common Lisp. Elle
est pourvue d'un ensemble d'abstractions permettant de décrire des traitements
génériques (sans connaissance préalable sur la nature des images cibles) et
d'un ensemble d'algorithmes prédéfinis basés sur ces abstractions. Il est
évidemment possible d'écrire de nouveaux algorithmes. Elle offre également un
DSL (Domain Specifique Language) pour la déclaration de chaînes complexes de
traitement et une interface graphique pour la programmation visuelle de ces
mêmes chaînes.
Le haut niveau d'abstraction de la bibliothèque a un impact non négligeable
sur les performances. +
Climb est une bibliothèque de traitement d'image écrite en Common Lisp. Elle
est actuellement pourvue d'une interface graphique permettant de concevoir des
chaînes de traitement d'images (Cf. capture d'écran) visuellement et à la
souris, c'est-à-dire sans avoir besoin de recourir à de la programmation. Ceci
est particulièrement utile pour des « clients » non informaticiens.
L'interface en question a été développée assez rapidement pour des besoin de
démonstration, mais n'est pas une solution satisfaisante sur le long
terme. L'interface elle-même est limitée en fonctionnalités, peu ergonomique,
pas très aguichante ni bien intégrée avec les différentes plateformes. De
plus, Gtk2 est un toolkit ancien dont la couche d'interfaçage avec Lisp n'est
plus vraiment maintenue. +
The Spot library (https://spot.lrde.epita.fr/) written in C++11 offers several
algorithms and data structures to build model checkers. Such a tool
checks whether the model of a system meets a given specification.
One way to perform this verification is to encode both the specification
and the model as omega-automata, build the synchronous product
of the two previous automata and finally check wether the product
automaton has an empty language. This last operation is called
an emptiness check and deals with automata of millions of
states and transitions.
Recently many parallel emptiness checks have been proposed, each of
them having strengths an weakness. Nonetheless it is still unknown if one
of them outperform the others. Indeed, since all these algorithms are implemented
in different tools, a fair comparison is impossible. +
Le stage proposé s’inscrit dans la thématique “reconnaissance des formes” du laboratoire. Le contexte est
l’analyse d’images ou de séquences d’images vidéos contenant des éléments de texte. L’extraction automatique
de texte dans des images naturelles ou des vidéos est une fonction essentielle dans de nombreuses applications,
notamment l’indexation automatique de documents ou photographies, la dématérialisation de documents,
l’assistance aux personnes malvoyantes, etc.
Le sujet proposé a pour objet la reconnaissance de texte dans les images naturelles. Des techniques de
localisation automatique de texte ont déjà été développées au LRDE. Nous souhaitons maintenant être capable
de reconnaître le texte extrait. Il existe déjà des logiciels capables de reconnaître du texte (O.C.R) mais ces
logiciels ne sont pas prévus pour le contexte des images naturelles. Les difficultés que présentent ce type
d’images (déformation perspective, défauts d’illumination...) rendent la reconnaissance difficile.
Plusieurs pistes seront explorées, tant sur les descripteurs, que sur les outils de classification. +
Le langage Lisp dispose de mécanismes pour la documentation du
code (les « docstrings ») et pour l'introspection, permettant ensemble
d'extraire suffisamment d'information pour générer des manuels de
références automatiquement. Par ailleurs, un système nommé QuickLisp
consistue aujourd'hui le standard de-facto pour le téléchargement et la
gestion de distributions de bibliothèques.
En combinant ces deux idées, il devient envisageable de fournir une
plateforme de documentation plus ou moins globable du monde Lisp,
générée automatiquement. +
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.
Omega-automata are used to represent languages over infinite words. These automata can be defined using numerous acceptance conditions such as Büchi, co-Büchi, Rabin, Streett, Parity, etc. Spot actually supports these acceptances condition in a generic way and allow them to be combined as desired. +
The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.
The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample). +
Mots-clefs :
* polymorphisme paramétrique
* programmation générique
* C++
* structures de données et interfaces
* génie logiciel
* traitement d'images. +
Les langages de programmation généraux fournissent tous un certain nombre de
types natifs tels les entiers, flottants, chaînes de caractères etc., des
agrégats niveau utilisateur comme les structures ou les classes des languages
oritentés-objet, et finalement des types de séquences tels les listes,
vecteurs ou tableaux multi-dimensionnels.
Dans un langage dynamiquement typé, il est possible de manipuler des séquences
hétérogènes, c'est-à-dire dont les éléments sont potentiellement de types
différents. Par exemple, la liste (1.5 "foobar" t) est une séquence hétérogène
contenant un entier, une chaîne de caractères et un symbole. Partant de là, la
question du typage de ces séquences se pose: si une séquence suit un motif
particulier de type pour ses éléments, comment exprimer le type de toutes les
séquences suivant ce même motif ?
Une réponse possible à cette question consiste à utiliser un formalisme proche
des expressions rationnelles, que nous appelons « expressions rationnelles de
types ». Par exemple, le type (int . string+ . symbol) pourrait représenter
l'ensemble de toutes les séquences commençant par un entier, contenant ensuite
une ou plusieurs chaînes de caractères, et terminées par un symbole.
Un tel système a été implémenté pour le langage Common Lisp. Ce système
contient un moteur (une machine à états) permettant de détermniner si une
séquence est conforme à un type hétérogène, et s'intègre dans le mécanisme de
typage du langage afin d'en produire une extension déclarative. +
The Spot library (https://spot.lrde.epita.fr/) written in C++14 offers several
algorithms and data structures to build model checkers. Such a tool
checks whether the model of a system meets a given specification.
One way to perform this verification is to encode both the specification
and the model as omega-automata, build the synchronous product
The model-checking process takes a model of a system and a LTL formula to check, and outputs either "correct" if the property holds, or a run of the system on which the property does not hold (a counterexample). +