We are happy to announce that the following paper has been
accepted for publication at the 5th International Workshop on
Verification and Evaluation of Computer and Communication
Systems (VECoS'11) that will take place in Tunis, Tunisia, on
September 15-16, 2011.
LTL Translation Improvements in Spot
A. Duret-Lutz
Laboratoire de Recherche et Développement de l'Epita (LRDE)
http://publis.lrde.epita.fr/201109-VECOS
Spot is a library of model-checking algorithms. This paper
focuses on the module translating LTL formulæ into automata. We
discuss improvements that have been implemented in the last four
years, we show how Spot's translation competes on various
benchmarks, and we give some insight into its implementation.
--
Alexandre Duret-Lutz
Hello,
I'm happy to announce that I will be writing a chapter for an upcoming
book on Domain Specific Languages. The chapter description is given
below:
Extensible languages -- blurring the distinction between DSLs and GPLs
Domain-specific language (DSL) design and implementation is inherently a
transversal activity. It usually requires from the application
developers knowledge and expertise in both the application domain and in
language design and implementation, two completely orthogonal areas of
expertise. The difficulty is that either one needs to find people with
such dual competence, which is rare, or one needs to add manpower to the
project by means of different teams which in turn need to coordinate
their efforts and communicate together, something not easy to do either.
>From the programming language perspective, one additional complication
is that being an expert developer in one specific programming language
does not make you an expert in language design and implementation --
only in using one of them. DSLs, however, are most of the time
completely different from the language in which the embedding
application is written. A general-purpose programming language (GPL),
suitable to write a large application, is generally not suited to
domain-specific modeling, precisely because it is too general. Using a
GPL for domain-specific modeling would require too much expertise from
the end-users and wouldn't be expressive enough for the very specific
domain the application is supposed to focus on.
As a consequence, it is often taken for granted that your application's
DSL has to be completely different from your application's GPL. But what
if this assumption was wrong in the first place ?
The need for designing a DSL as a completely new language often comes
from the lack of extensibility of your GPL of choice. By imposing a
rigid syntax, a set of predefined operators and data structures on you,
the traditional GPL approach gives you no choice but to implement your
application's DSL as a different language, with its own lexical and
syntactic parser, semantic analyzer and possibly its own brand new
interpreter or even compiler.
A much less widely accepted view, however, is that some GPLs are
extensible, or customizable enough to let you implement a DSL merely as
either a subset or an extension of your original language. The result is
that your final application, as a whole, is now written in a completely
unified language. While the end-user does not have access to the whole
backstage infrastructure and hence does not really see a difference with
the traditional approach, the gain for the developer is substantial.
Since the DSL is now just another entry point for the same original GPL,
there is essentially only one application written in only one language
to maintain. Moreover, no specific language infrastructure (parser,
interpreter, compiler etc.) is required for the DSL anymore, since it is
simply expressed in terms of the original GPL. The already existing GPL
infrastructure is all that is needed.
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
Bonjour,
nous avons le plaisir de vous présenter le n°21 du bulletin du LRDE.
C'est un numéro spécial consacré au séminaire des élèves CSI organisé le
4 juillet 2011 avec les résumés de toutes les présentations. Les
étudiants des promos 2012 et 2013 y présenteront leur travail.
Vous trouverez également les dernières publications et sorties de
logiciels du LRDE dans ce numéro.
Et une autre date à retenir : le 6 juillet aura lieu le séminaire LRDE.
Vous pouvez télécharger le bulletin en couleur à la page suivante :
http://publis.lrde.epita.fr/201107-l-air-de-rien-21
--
Daniela Becker
Responsable administrative du LRDE
Bonjour,
nous avons le plaisir de vous inviter au séminaire des étudiants du
LRDE. Il aura lieu le lundi 4 juillet 2011 à 9h30 - 17h15 en Amphi
Masters (KB).
-----------------------------------------------------------------------
Au programme:
*CLIMB, SCRIBO, TIGER, SPOT, SPEAKER ID et VAUCANSON*
http://publis.lrde.epita.fr/Seminar-2011-07-04
CLIMB
* 09h30 : Arbres de composantes et opérateurs de chaînage -- Christopher
Chedeau
* 10h00 : Ecriture d'algorithmes de traitement d'images génériques --
Simon Guillot
* 10h30 : Implémentation de voisinages pondérés -- Laurent Senta
SCRIBO
* 11h15 : Analyse de la mise en page d'un document dans SCRIBO -- Julien
Marquegnies
* 11h45 : Extraction du texte en inverse video dans SCRIBO -- Coddy Levi
* 12h15 : Désambiguïsation de la superposition de lignes -- Sylvain Lobry
TIGER
* 14h00 : Optimisations dans le compilateur Tiger -- Félix Abecassis
SPOT
* 14h30 : Amélioration de la dégénéralisation dans Spot -- Pierre Parutto
* 15h00 : Réductions basées sur la bisimulation appliquées aux TGBA --
Thomas Badie
SPEAKER ID
* 15h45 : Speaker ID - Détection de voix -- Victor Lenoir
VAUCANSON
* 16h15 : Avancées vers Vaucanson 1.4 et 2.0 -- Guillaume Fiette
* 16h45 : Implémentation du semi-anneau rationnel -- David Moreira
-----------------------------------------------------------------------
Les Résumés des exposés :
**************************
CLIMB
09h30 : Arbres de composantes et opérateurs de chaînage -- Christopher
Chedeau
Climb est une bibliothèque de traitement d'images générique ayant pour
objectif le prototypage rapide. L’implémentation de deux algorithmes
d’arbre de composantes impacte Climb de plusieurs façons : la définition
des valeurs est étendue, de nouveaux ensembles de sites sont ajoutés et
les outils de développement sont améliorés. Un détour est pris afin de
comprendre le patron de conception de chaînage popularisé par la
bibliothèque jQuery. La méthode est modifiée afin de s’adapter au
traitement d’images ainsi qu’à Common Lisp. Elle est également étendue
via une notation parallèle ainsi qu’avec une meilleure gestion du fil
d’exécution.
10h00 : Ecriture d'algorithmes de traitement d'images génériques --
Simon Guillot
Climb est une bibliothèque générique de traitement d'images en Lisp.
L'étude de l'implémentation d'un algorithme de segmentation par ligne de
partage des eaux permet de faire état des possibilités offertes par un
langage dynamique tel que Lisp allié à une modélisation générique des
images. Cette étude de cas permet d'aborder les concepts de base de la
manipulation d'images au sein de Climb tels que les sites, les ensembles
de sites et les accumulateurs. L'utilisation de l'ensemble de ces
notions reposent sur l'aspect dynamique et fonctionnel de Lisp.
10h30 : Implémentation de voisinages pondérés -- Laurent Senta
Climb est une bibliothèque de traitement d’images générique développée
en Lisp. Les voisinages sont representés sous la forme d’ensemble de
sites (site-set) pour permettre des manipulations génériques sur de
multiples types d’images. En parallèle de ces concepts, une étude des
voisinages pondérés est effectuée, expliquant différents moyens
d’étendre le concept d’une écriture unique des algorithmes pour les
exécuter sur différents types de paramètres. Trois implémentations sont
proposées, décrites et comparées au niveau de leur généricité et de leur
expressivité.
SCRIBO
11h15 : Analyse de la mise en page d'un document dans SCRIBO -- Julien
Marquegnies
L’extraction des différentes structures d’un document numérisé se base
sur la mise en place d’une chaîne de traitement constituée d’un certain
nombre d’étapes primordiales afin d’optimiser la qualité du rendu final.
L’étude de la mise en page du document, à savoir la localisation des
lignes de texte et des paragraphes, constitue le coeur même de la chaîne
puisque le rendu obtenu est étroitement corrélé avec les zones de texte
données en entrée à l’OCR. Ainsi, nous présenterons une méthode hybride
d’analyse de mise en page développée dans le cadre du projet SCRIBO.
11h45 : Extraction du texte en inverse video dans SCRIBO -- Coddy Levi
L'extraction du texte d'images de document intervient dans le processus
plus général de compréhension de documents que propose le projet SCRIBO.
Le texte peut être présent dans deux formes : foncé sur fond clair ou
clair sur fond foncé, appelé Inverse Video. Cette présentation explique
les problématiques liées à l’extraction du texte en inverse video dans
SCRIBO en utilisant la chaîne de traitement déjà existante, les
problèmes ainsi introduits et les pistes explorées pour l’amélioration
des résultats.
12h15 : Désambiguïsation de la superposition de lignes -- Sylvain Lobry
Lorsque l'on essaye d'extraire du texte en inverse vidéo (couleur claire
sur fond fonce), nous verrons lors de la présentation de Coddy Levi que
de nombreux problèmes surgissent. Le plus courant d'entre eux est la
superpositions entre ce texte en inverse vidéo, et celui en couleur
foncée sur clair. Nous montrerons donc lors de cette présentation
comment faire un choix entre ces lignes en superposition, en considérant
différents critères et en les pondérant.
TIGER
14h00 : Optimisations dans le compilateur Tiger -- Félix Abecassis
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 relégué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.
SPOT
14h30 : Amélioration de la dégénéralisation dans Spot -- Pierre Parutto
Spot est une bibliothèque de model checking developée au LRDE. Sa force
est d’utiliser les Automates de Büchi Generalisés basés sur les
transitions (TGBA), plutôt que les Automates de Büchi basés sur les
Transitions (TBA) très utilisés dans les autres model checkers. Les TGBA
nous permettent de produire des automates très petits représentant une
formule rendant toutes les étapes suivantes du model checking plus
rapide. Comme Spot met l’accent sur l’utilisabilité et la
personnalisation des outils, une attention particulière est portée sur
l’interfaçage avec d’autres programmes. La capacité de transformer un
TGBA en TBA (appelé dégénéralisation) sans perdre en performance est
donc centrale. Cette présentation a pour but de montrer une analyse des
outils de dégénéralisation présents dans Spot et de proposer des moyens
pour les améliorer.
15h00 : Réductions basées sur la bisimulation appliquées aux TGBA --
Thomas Badie
Spot est une bibliothèque C++ de model checking utilisant l’approche par
automates. Pour représenter les propriétés à vérifier, nous utilisons
des formules LTL qui sont traduites en automates. Dans Spot, ces
automates sont des Automates de Büchi généralisés basés sur les
transitions (TGBA). Un enjeu pour tout model checker, est d’être rapide.
Une manière de faire est de rendre les automates aussi petit que
possible. La littérature scientifique propose de nombreux algorithmes
pour arriver à notre but. La bisimulation et la simulation réduisent des
automates qui reconnaissent des mots infinis. Ce rapport montre comment
adapter ces algorithmes pour des TGBA ainsi que le gain apporté par
l’implémentation de la bisimulation, ce qui souligne l’importance
d’implémenter la simulation pour réduire les TGBA.
SPEAKER ID
15h45 : Speaker ID - Détection de voix -- Victor Lenoir
La détection de voix a de nombreuses applications. C'est par exemple une
étape obligatoire avant de faire de la reconnaissance du locuteur. Ce
rapport présente deux différents types d'algorithmes pour la détection
de voix (VAD) : un utilisant des seuils et le second utilisant des
mélanges de gaussiennes (GMM). Les algoritmes proposés utilisent des
caractéristiques calculées sur des petits intervalles de temps comme par
exemple l'énergie, la monotonie spectrale ou les Mel-Frequency Cepstral
Coefficients (MFCC). Les différents algorithmes de détection de voix
sont comparés dans différentes conditions de bruit afin de mettre en
évidence leur robustesse aux bruits.
VAUCANSON
16h15 : Avancées vers Vaucanson 1.4 et 2.0 -- Guillaume Fiette
Vaucanson est une plateforme de manipulation d’automates finis et de
transducteurs. Après plusieurs années de developpement, il fût constaté
que l’interface mise en place pour manipuler les automates était trop
complexe. Des travaux furent donc entrepris pour résoudre ce problème,
amenant ainsi à l’introduction des "label kinds". Deux versions de la
plateforme sont donc en developpement aujourd’hui : Vaucanson 1.4, qui
vise à terminer et compléter le travail effectué avant l’introduction
des kinds et Vaucanson 2.0, dernière version de la plateforme, pour le
moment incomplète. Ce rapport a pour but de présenter une nouvelle
fonctionnalité de Vaucanson 1.4, les semi-anneaux Z/nZ, ainsi que le
travail en cours sur Vaucanson 2.0.
16h45 : Implémentation du semi-anneau rationnel -- David Moreira
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és entrepris afin d’introduire
le concept de kind d’un automate dans la bibliothèque. Aujourd’hui, une
partie de la nouvelle interface a été implémentée et le travail sur le
cœur a laissé Vaucanson 1.4 dans un état instable. Ce rapport montrera
dans un premier temps le travail effectué pour Vaucanson 1.4, puis sur
les travaux entrepris afin de rendre stable Vaucanson 2.0.
--
Daniela Becker
Hello,
I'm pleased to announce that my proposal for Common Lisp "File-Local
Variables" has been accepted, finalized and published at the Common
Document Repository. It can now be referred to as CDR #9.
The abstract is given below:
The Common Lisp standard defines two special variables, *PACKAGE* and
*READTABLE*, that are treated in a special way: the functions LOAD and
COMPILE-FILE establish a new dynamic binding for each of them, so that
any modification to their value at load or compile time becomes local to
the file being processed. It is this particular treatment of these
variables that allows for IN-PACKAGE or IN-READTABLE (from the
NAMED-READTABLES library) to essentially have a ``file-local'' effect.
The motivation for the present document is the claim that this behavior
could be useful for other, user-defined variables, although there is
currently no way to do so in standard Common Lisp.
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
We are happy to announce that the following paper has been accepted
for publication at the 9th international symposium on Automated
Technology for Verification and Analysis (ATVA'11) that will take
place in Taipei, Taiwan, on October 11-14, 2011.
Self-Loop Aggregation Product — A New Hybrid Approach to
On-the-Fly LTL Model Checking
A. Duret-Lutz (1)
K. Klai (2)
D. Poitrenaud (3)
Y. Thierry-Mieg. (3)
(1) Laboratoire de Recherche et Développement de l'Epita (LRDE)
(2) Laboratoire d'Informatique de Paris-Nord (LIPN)
(3) Laboratoire d'Informatique de Paris 6 (LIP6)
http://publis.lrde.epita.fr/201110-ATVA
We present the Self-Loop Aggregation Product (SLAP), a new hybrid
technique that replaces the synchronized product used in the
automata-theoretic approach for LTL model checking. The proposed
product is an explicit graph of aggregates (symbolic sets of states)
that can be interpreted as a Büchi automata. The criterion used by
SLAP to aggregate states from the Kripke structure is based on the
analysis of self-loops that occur in the Büchi automaton expressing
the property to verify. Our hybrid approach allows on the one hand to
use classical emptiness-check algorithms and build the graph
on-the-fly, and on the other hand, to have a compact encoding of the
state space thanks to the symbolic representation of the
aggregates. Our experiments show that this technique often outperforms
other existing (hybrid or fully symbolic) approaches.
--
Alexandre Duret-Lutz
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 6 juillet 2011 (14h-15h).
Au programme:
* 14h: Un algorithme rapide pour le Compressive Sensing sur
architectures parallèles
-- Alexandre Borghi
http://www.lri.fr
Dans ce séminaire je présenterai un algorithme de résolution approchée
pour le problème du Compressive Sensing basé sur la programmation
convexe. Cet algorithme a la particularité d'avoir été pensé dès sa
conception pour tirer partie des architectures matérielles modernes, ce
qui permet une implémentation efficace et rapide sur ces celles-ci. Bien
qu'une résolution approchée soit en pratique suffisante pour obtenir
rapidement une solution de très bonne qualité, une variante exacte très
rapide sera aussi présentée. Cette dernière n'est toutefois utilisable
que sous certaines conditions. Trois types d'architectures parallèles
sont ici envisagées : des processeurs multi-coeurs avec unités de calcul
vectoriel, des processeurs graphiques (GPU) et le processeur Cell.
-- Alexandre Borghi est diplômé de la promotion CSI 2007 de l'EPITA et
effectue actuellement sa thèse au LRI de l'Université Paris-SUD XI. Il
s'intéresse principalement à l'adaptation de l'algorithmique aux
architectures parallèles.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://www.lrde.epita.fr/mailman/listinfo/seminaire
Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 15 juin 2011 (14h-17h).
Au programme:
* 14h: Modèle basé-contexte pour l'annotation automatique du multimédia
-- Nicolas Ballas
http://www.kalisteo.fr/en/index.htmhttp://caor.mines-paristech.fr/
Ces dernières années ont vu exploser le nombre de vidéos disponibles sur
internet. Pour permettre leur exploitation, il est nécessaire de mettre
en place des systèmes analysant automatiquement ces données multimédia.
De tels systèmes permettent notamment d'indexer automatiquement des
vidéos en fonction de leurs contenus. Durant cette présentation, je
m'intéresserai aux récentes avancées effectuées dans ce domaine. Je
présenterai des descripteurs vidéos, développés dans le cadre de ma
thèse, qui capturent le mouvement et l'apparence d'une vidéo pour les
résumer dans une courte signature. Ces signatures peuvent être utilisées
a posteriori pour détecter différents évènements ou concepts dans les
vidéos.
-- Nicolas Ballas effectue sa thèse entre le laboratoire LVIC du CEA/List
et le laboratoire CAOR de l'école des Mines de Paris. Il s'intéresse
principalement au problème de perception automatique à travers l'étude
d'algorithmes combinant vision par ordinateur et apprentissage
automatique.
* 15h30: Traitement d'images sur processeur graphique avec CUDA et C++
-- Matthieu Garrigues
http://uei.ensta-paristech.fr
Conçus à l'origine pour le rendu 2D et 3D, les processeurs graphiques
(GPU) peuvent aujourd'hui être considérés comme des processeurs
génériques massivement parallèles. Mais ce parallélisme impose des
contraintes sur les algorithmes implantés et les types de données
utilisés. D'autre part, le bus de communication entre le processeur
central (CPU) et le GPU peut être un goulot d'étranglement.
Ce séminaire débutera par un aperçu des avantages et inconvénients de la
programmation GPU, puis je présenterai l'implantation d'un algorithme
temps réel de suivi de points dans une vidéo. Je terminerai par
l’introduction de deux petites boîtes à outils : Cuimg et Dige. Cuimg
utilise C++ pour simplifier l'écriture d'algorithmes de traitement
d'images avec CUDA, tandis que Dige, basée sur le framework Qt, permet
le prototypage rapide d'interfaces graphiques.
-- Matthieu Garrigues est diplômé de la promotion CSI 2009 de l'EPITA.
Depuis, il s'intéresse au développement et l'implantation d'applications
de vision par ordinateur sur des architectures parallèles. Il est
actuellement ingénieur de recherche à l'unité d'électronique et
d'informatique de l'ENSTA.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://www.lrde.epita.fr/mailman/listinfo/seminaire
We are happy to announce that the following paper has been accepted
for publication at the 2nd International Workshop on Scalable and
Usable Model Checking for Petri Nets and other models of Concurrency
(SUMo'11) that will take place in Newcastle, UK, on June 21, 2011.
Generalized Büchi Automata versus Testing Automata
for Model Checking
A.-E. Ben Salem (1&2)
A. Duret-Lutz (1)
F. Kordon (2)
(1) Laboratoire de Recherche et Développement de l'Epita (LRDE)
(2) Laboratoire d'Informatique de Paris 6 (LIP6)
http://publis.lrde.epita.fr/201106-SUMO
Geldenhuys and Hansen have shown that a kind of omega-automaton
known as testing automata can outperform the Büchi automata
traditionally used in the automata-theoretic approach to model
checking. This work completes their experiments by including a
comparison with generalized Büchi automata; by using larger state
spaces derived from Petri nets; and by distinguishing violated
formulae (for which testing automata fare better) from verified
formulae (where testing automata are hindered by their two-pass
emptiness check).
--
Alexandre Duret-Lutz
We are happy to announce that the following paper has been accepted
for publication at the 11th International Conference on Document
Analysis and Recognition (ICDAR) that will take place at Beijing, China,
on September 18 - 21, 2011:
Guillaume Lazzara (1), Roland Levillain (1), Thierry Géraud (1),
Yann Jacquelet (1), Julien Marquegnies (1), Arthur Crépin-Leblond (1)
A Free Software Framework
for Document Image Analysis
http://publis.lrde.epita.fr/201109-ICDAR
(1) EPITA Research and Development Laboratory (LRDE)
Electronic documents are being more and more usable tanks to better and
more affordable network, storage and computational equipment. But in
order to benefit from computer-aided document management, paper
documents must be digitized and analyzed. This task may be challenging
at several levels. Data may be of multiple types thus requiring
different adapted processing chains. The tools to be developed should
also take into account the needs and knowledge of users, ranging from a
simple graphical application to a complete programming framework.
Finally, the data sets to process may be large. In this paper, we expose
a set of features that a Document Image Analysis framework should
provide to address the previous issues. These ideas are implemented as
an open source module built on top of a generic and efficient image
processing platform. Our solution features services such as
preprocessing filters, text detection, page segmentation and document
reconstruction (as XML, PDF or HTML documents). This framework, composed
of reusable software components, can be used to create full-fledged
graphical applications, small utilities, or processing chains to be
integrated into third-party projects.