Job objectives
From LRDE
This is a property of type Text.
J
Bison generates parsers for a given grammar. In some case, one is interesting in parsing different aspects of a grammar (for instance, "parse this expression", or "parse this declaration", or "parse this program"). There is no built-in support for this in Bison. It is however easy to implement. The internship consists in adding this feature in the front-end (i.e., find a means for the user to declare that she wants to have several "entry points"), and in the back-ends (i.e., prepare Java, C, and C++ parsers with the needed support: typically generating a "parse_foo()" function for each "foo" entry-point). There are many other things to develop in Bison, this is just an initial assignment: more will come as the first one is properly addressed.
(i) Sort the error messages: Bison has several passes, and each pass generates its own error messages. As a result, there is sometimes an error on line 3, then on line 2 and then on line 1. Sort them to issue them in a more natural order; (ii) Colorize the diagnostics: Today compiles such as GCC or clang issue messages in color. Do that in Bison too ; (iii) Optimize the generator parsers: Currently Bison aims at producing small parsers (small tables). It might be interesting to release some of these optimizations (since nowadays we have much more memory available) to see if we gain some speedup. That would result in a -O option, as in compilers (with -Os, -O2, etc.). +
La bibliothèque Spot fournit des algorithmes pour fabriquer un model checker, c'est-à-dire un outil qui sert à prouver que tous les comportements possible d'un système vérifient une propriété donnée. On y trouve entre autres des algorithmes pour traduire des formules de logique temporelle (qui expriment les propriétés) en automates (pour automatiser la preuve). L'une de ces logiques s'appelle PSL (Property Specification Language) et est déjà supportée, mais de façon sous optimale. L'objectif du stage est de réimplementer la traduction de PSL en automates proprement. Cela passe par l'introduction d'un nouveau type d'automate, similaire aux automates non-déterministes du cours de THLR, mais avec des transitions finales au lieu d'avoir des états finaux. Comme il existe déjà une traduction, et que Spot est déjà équippé avec tout ce qu'il faut pour comparer des traductions entre elles, il sera facile de rapidement débugger la nouvelle approche. +
Des planches ici : http://www.lrde.epita.fr/~theo/private/phd/TheseHolographie.pdf
Des vidéos ici : http://www.youtube.com/channel/UC_DamX84B2Y375nANrD_Tjw
L'objectif de la thèse proposée sera donc de développer des algorithmes efficaces pour l'acquisition, l'analyse et le traitement en temps réel des séquences hyperspectrales holographiques pour l'imagerie rétinienne. Les données seront acquises par plusieurs types de caméras d'au moins 1 Giga octet/s de bande passante. Les reconstructions numériques et l'affichage d'hologrammes se feront sur GPU NVIDIA. Le logiciel permettra la reconstruction d'hologrammes à la cadence d'acquisition des caméras CMOS les plus rapides de l'état de l'art, afin de permettre d'exploiter leur bande passante d'acquisition pour l'imagerie hyperspectrale.
Cette thèse a pour objectif la conception de méthodes de calcul en imagerie hyperspectrale holographique et la réalisation d'un logiciel d'imagerie à très haut débit pour un instrument d'imagerie médicale à l'hôpital des 15-20. Une très bonne maîtrise du C++ et des connaissances en traitement d'images et/ou en « machine learning » sont requises. La connaissance de CUDA est un plus. +
The objective of this internship is to improve the performances of Vcsn in every possible ways. This includes:
* design of a binary format to save and restore automata (possibly with mmap)
* improvements to the core data structures
* design of efficient alternatives to classical data structures such as found in the C++ library
* improvement of the existing algorithms taken from Automata Theory, such as epsilon-transition removal
* optimization of the ''dyn'' type-erased dynamic dispatch
* development of benches and comparison with other platforms
* etc. +
The goal of the internship is to improve the last two points (Python bindings and web interface): we would like to access all features of Spot from Python (and in particular from IPython), and on top of this Python interface, we would like more online services that people can use without having to install Spot. +
Presently, our first implementation saves the SAT problem as a huge file before calling the SAT-solver, and it does
this for each iteration. The goal of this internship is to improve this situation in multiple ways:
* implement purely technical optimizations (like direct communication with the SAT solver, bypassing any temporary files)
* take advantage of features offered by modern SAT solvers (for instance an "incremental SAT-solver" can be given new constraints after it has found a solution, without needing to restart from scratch)
* implement optimizations to the encoding of the SAT-problem, based on structural properties of the automaton (we have some ideas)
In a second step, we would like to generalize the existing technique to non-deterministic automata (first as input, and then as output as well). +
The purpose of this internship is to (begin to) fill the gap by adding Lisp to the comparative literature. The work will consist in the study of literature demonstrating some useful approaches for the design of DSLs, further it should propose an alternative approach with Lisp and then compare the results. The steps of this training will include:
* Familiarization with Common Lisp and in particular its extensibility capabilities.
* Getting acquainted with the literature on the design and implementation of DSLs in other languages.
* Choice of an application-centric approach or a comparative approach based on this literature and implementation of a Lispish equivalent.
* Finally, analysis of the results following the aspects such as: ease of implementation, expressiveness, performance etc. . +
The goal of this internship is to study how to port a particular application of R to an equivalent one in Common Lisp. The first objective (which is certain) is to achieve a much higher level of performance than that of the original application. The long term goal is to consider a new implementation of R (or of a subset of R) over Common Lisp, with the intuition that it will result in a much simpler and better system, which is in addition much more efficient. +
* theory: 10%
* bibliography: 20%
* exploration: 40%
* implementation and tests: 30%
+
Goal:
Work:
* theory: 20%
* bibliography: 10%
* exploration: 30%
* proof design: 30%
* implementation and tests: 10% +
* theory: 10%
* bibliography: 10%
* exploration: 30%
* algorithm design: 30%
* implementation and tests: 20%
+
L'objectif de ce stage est d'étudier en détail le comportement de la
bibliothèque vis-à-vis des performances, d'en fournir une analyse critique et
constructive puis de proposer des idées d'optimisation. Même si certains
centres de coûts sont bien connus ou prévisibles (par exemple le dispatch
dynamique de la couche objet), il reste capital de disposer d'une vision
précise de la répartition de ces coûts afin par la suite de se livrer à des
optimisations pertinentes. Aujourd'hui, la bibliothèque est utilisée comme une
platforme expérimentale pour l'étude de différents paradigmes de programmation
générique. L'un des intérêts du language Lisp, hautement réflexif, est qu'il
donne accès non seulement à de nombreux paradigmes de programmation, mais
également à l'implémentation de ceux-ci. Il est donc possible d'analyser non
seulement l'impact des paradigmes utilisés sur les performances, mais
également l'impact de leur implémentation. Dans une optique d'optimisation, il
sera donc possible d'aller jusqu'à faire évoluer l'infrastructure sous-jacente
au langage lui-même.
Déroulement du stage:
- découverte du langage Lisp et de la bibliothèque Climb,
- profiling de la bibliothèque et analyse des résultats,
- expérimentations sur toute idée d'optimisation qui pourra surgir, suite à l'analyse précédente. +
L'objectif de ce stage est la poursuite d'un travail déjà entamé: concevoir, en s'inspirant de l'interface
existante, une nouvelle interface plus moderne et foncionnelle basée sur
Qt. L'utilisation de Qt permettra notamment d'obtenir un « look & feel » natif
sur toutes les plateformes (OS X, Linux etc.). D'autre part, les solutions
d'interfaçage entre Lisp et Qt sont aujourd'hui de meilleure qualité que
celles pour Gtk.
Déroulement du stage:
- apprentissage des bases de Qt
- découverte du langage Lisp, de la bibliothèque Climb et de l'interface pour Qt,
- poursuite de l'écriture de la nouvelle interface à fonctionnalités équivalentes à l'ancienne,
- en fonction du temps et au libre choix du stagiaire: toute amélioration de l'interface elle-même, de son intégration avec le reste de la bibliothèque etc. +
The goal of this internship is:
* to implement optimized scalable versions of state-of-the-art emptiness checks
* to evaluate relative performances of each of them
* to help in the development of the thread-safe part of the Spot library by adding concurrent (possibly lock-free) data structures and algorithms. +
À l'heure actuelle, il existe déjà une implémentation de cette idée:
quickdocs.org. Cependant, la documentation fournie est assez
rudimentaire. D'un autre côté, je suis l'auteur de Declt, un système de
génération automatique de manuels de références beaucoup plus complet,
mais ce système produit de la documentation bibliothèque par bibliothèque,
sans plateforme centralisée. L'idée serait donc de s'inspirer de
quickdocs.org pour développer un nouveau site, quickrefs.org, basé sur
Declt. +
The goal is to implement several algorithms that transform automata using one acceptance condition into automata using another acceptance condition. Some of these conversions are essential to some decision procedures.
For instance, we currently have an implement of Krishnan's algorithm for converting a deterministic Rabin automata into an equivalent deterministic Büchi automaton when such an automaton exist. We believe the procedure could be extended to handle deterministic "Generic Rabin" as input. Implementing such a new transformation would give us an efficient way to decide whether some LTL formula is realizable by a deterministic Büchi automaton, because we can already transform LTL into generic Rabin. +
We wish to build an interactive, web-based demonstration prototype for Spot, to illustrate the interest of model checking.
The targeted use-case is the verification of a controller for lifts.
The prototype should provide several functionalities, among which:
* a graphical representation of the system and its evolution,
* a way to specify a controller and to check temporal properties by calling Spot.
* the capability to replay (graphically) a counter-example given by Spot.
* the ability to describe the characteristics of the lifts system (number of lifts, ranges etc.)
Such a prototype is intended to be used in the communication of the LRDE, for example during the Journées Portes Ouvertes.
Another module would consist in a game on LTL.
The game picks a LTL formula (at random, or among a list of pre-selected patterns), and displays a corresponding omega-automaton to the player.
The goal is to find the original LTL formula.
When the player makes a wrong guess, the game could help her with traces recognized by the secret formula but not by the player's formula. +
Dans le cadre du calcul scientifique, on a besoin d'outils performants sachant que l'on dispose souvent de gros volumes de données. Les algorithmes qui traitent les données manipulent généralement des abstractions du domaine. En effet, derrière les notions de matrice, de graphe, d'image, etc. se cachent plusieurs implémentations de ces structures. On souhaite pouvoir conserver la forme intrinsèquement abstraite des algorithmes, tout en garantissant que cela n'induit pas
de surcoût à l'exécution. Dit autrement, on veut que les algorithmes soient les plus rapides possibles, bien qu'ils aient à traiter des données de types différents. Pour cela, la programmation générique est une solution.
Le but de ce stage est de montrer comment les fonctionnalités offertes par les dernières normes du C++ permettent de faciliter l'écriture d'outils génériques. Le domaine d'application sera une bibliothèque de traitement d'images. +
L'objectif de ce stage est d'évaluer l'applicabilité de la notion d'expression
rationnelle de type à d'autres langages dynamiques que Lisp. Ce travail
comporte deux angles distincts. D'une part, l'implémentation d'un moteur
similaire à celui déjà écrit pour Lisp, et qui ne repose que sur de
l'introspection dynamique de type. Ceci ne doit pas poser de problème. D'autre
part, et c'est la partie la plus expérimentale, l'étude de l'insertion de ce
moteur dans le système de typage existant pour le ou les langages
choisis. Cette dernière partie dépendra des capacités constatés dans les
langages en question, et nous permettra de déterminer à quel point leurs
systèmes de typage sont extensibles.
Ce travail donnera certainement lieu à de la publication académique. +
We wish to build a distributed model-checker so that we can outcome the limitation (time and memory) of multithreaded algorithms.
The internship aims:
* to implement optimized scalable versions of state-of-the-art emptiness checks
* to evaluate relative performances of each of them
* to help in the development of the thread-safe part of the Spot library by adding distributed data structures and algorithms. +