Bonjour,
nous avons le plaisir de vous inviter au séminaire des étudiants-chercheurs du
LRDE. Il aura lieu le mercredi 3 juillet 2013 à partir de 9h30 en Amphi 3 (KB).
Et notez d'ores et déjà la date du jeudi 11 juillet où les étudiants CSI 2014 présenteront leurs
travaux.
-----------------------------------------------------------------------
Au programme du 3 juillet 2013 :
OLENA
* 09h30 : Analyse structurelle haut-niveau de document dans le module Scribo d’Olena -- Christophe Escobar
* 10h00 : Détection de logotypes et autres invariants caractéristiques -- Anthony Seure
SPEAKER ID
* 10h30 : Les Machines de Boltzmann dans la reconnaissance du locuteur -- Jean-Luc Bounthong
* 11h00 : Approximation de la distance entre i-vecteurs par Perceptron Multi-Couches -- Jimmy Yeh
CLIMB
* 11h45 : Maintenance automatique des symboles exportés dans les packages de Common Lisp – Christophe Vermorel
VAUCANSON
* 12h15 : Améliorer l’architecture de Vaucanson 2 -- Guillaume Sanchez
* 12h45 : Transducteurs dans Vaucanson 2 – Victor Santet
Les Résumés des exposés :
**************************
OLENA
* 09h30 : Analyse structurelle haut-niveau de document dans le module Scribo d’Olena -- Christophe Escobar
L’extraction de structures dans un document numérisé se base sur la mise en place d’une chaîne de traitements constituée de briques élémentaires. L’analyse haut-niveau d’un document nécessite des informations structurelles sur celui-ci et se basera donc sur cette chaîne de traitements. Elle consistera à extraire des informations plus abstraites de nature structurelle sur un document, pour obtenir des "indices" sur sa structure. À l’aide de ces indices et de schémas de structure, il est ensuite possible de réaliser des traitements de haut-niveau tels que l’identification du flot de lecture, l’extraction d’éléments spécifiques ou la reconstruction d’un document dans un autre format.
* 10h00 : Détection de logotypes et autres invariants caractéristiques -- Anthony Seure
La détection de logotypes et d’invariants dans une image a pour but de trouver parmi une ou plusieurs images un élément graphique qui caractérise une marque, entreprise, etc. De tels éléments peuvent se retrouver dans de nombreuses images naturelles mais également dans des images publicitaires. L’intérêt de l’intégration d’un tel outil dans Olena et Terra Rush permettrait de mieux indexer les contenus mais également d’invalider des zones de l’image dans d’autres chaînes de traitement. Nous expliquerons principalement une méthode générique permettant de localiser les points-clés invariants d’une image : les descripteurs SIFT.
SPEAKER ID
* 10h30 : Les Machines de Boltzmann dans la reconnaissance du locuteur -- Jean-Luc Bounthong
L’espace Total Variability (TV) représente actuellement l’état de l’art dans le domaine de la vérification du locuteur. Des progrès significatifs ont été réalisés grâce aux nouvelles méthodes de classification comme l’Analyse discriminante linéaire probabiliste (PLDA) ou la Distance Cosinus (CD). Dans cette étude, nous explorons une nouvelle méthode pour déterminer la distance entre deux i-vecteurs en utilisant une variante des Machines de Boltzmann, ces nouvelles approches ont montré des résultats satisfaisants dans le domaine du traitement d’images. Nous allons aussi comparer les performances en terme de fiabilité avec les méthodes classiques comme PLDA ou CD.
* 11h00 : Approximation de la distance entre i-vecteurs par Perceptron Multi-Couches -- Jimmy Yeh
Actuellement, l’espace des i-vecteurs est la représentation standard des paramètres de la parole dans les systèmes de reconnaissance du locuteur. Le calcul du score est généralement basé sur la distance cosinus, ou sur l’analyse discriminante linéaire probabiliste. Le but de ce sujet est de remplacer ces approches par un Perceptron Multi-Couches (PMC). Le PMC a montré en effet de bonnes performances pour approximer des fonctions non linéaires. L’idée principale étant de trouver une meilleure fonction que la distance cosinus. Les performances du PMC seront comparées aux autres méthodes comme la distance cosinus ou encore la machine de Boltzmann.
CLIMB
* 11h45 : Maintenance automatique des symboles exportés dans les packages de Common Lisp -- Christophe Vermorel
Les "packages" de Common Lisp offrent une fonctionnalité analogue aux espaces de noms présents dans des langages comme le C++. Ceux-ci permettent d’encapsuler des symboles qui peuvent être exportés ou privés. Les symboles exportés peuvent être explicitement déclarés lors de la définition du package. Cette liste de symboles est fastidieuse à maintenir lors du développement de projets de grosse envergure. Dans ce rapport, nous étudions des techniques de maintenance automatiques de cette liste. Plusieurs alternatives sont présentées et comparées.
VAUCANSON
* 12h15 : Améliorer l’architecture de Vaucanson 2 -- Guillaume Sanchez
Vaucanson 2 est la suite de Vaucanson, la plate-forme de manipulation d’automates finis. Ce redémarrage à zéro a été fortement encouragé par quelques problèmes de conception. Vaucanson 2 entend apprendre des erreurs de son prédecesseur, et dans ce but, un vrai travail de conception doit être fait. Les templates doivent être utilisés pour la performance (évitant un usage abusif de fonctions virtuelles) afin de pouvoir préférer la généricité plutôt que la généralité, tout en conservant une flexibilité lors de l’exécution. Vaucanson 2 prétendra aussi à une compilation dynamique de code (types d’automates et algorithmes) et de le charger en tant que bibliothèque dynamique. Ces simples problèmes amènent à des architectures de distribution complexes et d’effacement de type, qui doivent être testés dans un environnement simulé.
* 12h45 : Transducteurs dans Vaucanson 2 -- Victor Santet
Le projet Vaucanson 2 tient à offrir à ses utilisateurs une large variété de types d’automates, notamment les transducteurs. Ce rapport propose une implémentation de transducteurs génériques, qui peuvent accepter des automates étiquetés par des n-uplets de langages.
--
Daniela Becker
Responsable administrative du LRDE
Bonjour,
nous avons le plaisir de vous annoncer la sortie du n°27 du bulletin du LRDE.
C'est un numéro spécial dédié aux publications du LRDE. Vous y trouverez des
articles de conférences, de journaux, un chapitre de livre, un prix du meilleur article,
les nouvelles versions de Spot, et enfin notre nouveau projet FUI : LINX.
Nous y parlons également des mouvements parmi le personnel du LRDE.
Et vous pouvez d'ores et déjà noter les dates des prochains séminaires des étudiants-
chercheurs du LRDE : ils exposeront leurs travaux les 3 et 11 juillet 2013.
Vous pouvez télécharger le bulletin en couleur à la page suivante :
http://publis.lrde.epita.fr/201306-l-air-de-rien-27
--
Daniela Becker
Bonjour
J'ai le plaisir de vous annocer la publication de notre article
"Unsupervised Methods for Speaker Diarization: An Integrated and
Iterative Approach" sur la segmentation du locuteur dans la revue IEEE
Transaction on Audio, Speech and Language Processing. Vous pouvez le
trouver en avant première sur le site de ieexplore :
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6518171
Au passage l'autre article "Unsupervised Methods for Speaker
Diarization: An Integrated and Iterative Approach" publié il y a deux
ans dans la même revue
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=5545402 a
recu cette année le prix du best paper award de la société IEEE signal
processing
Bien cordialement
Réda
--
Réda DEHAK
We are happy to announce that the following two tool papers have been
accepted for publication at the 11th International Symposium on
Automated Technology for Verification and Analysis (ATVA'13) that will
take place in Hanoi, Vietnam, on 15-18 October 2013.
* LTL Model Checking with Neco
- Łukasz Fronc (IBISC, Université d'Évry/Paris-Saclay)
- Alexandre Duret-Lutz (LRDE, EPITA)
We introduce neco-spot, an LTL model checker for Petri net models. It
builds upon Neco, a compiler turning Petri nets into native shared
libraries that allows fast on-the-fly exploration of the state-space,
and upon Spot, a C++ library of model-checking algorithms. We show
the architecture of Neco and explain how it was combined with Spot to
build an LTL model checker.
http://publis.lrde.epita.fr/201310-ATVAb
* Manipulating LTL formulas using Spot 1.0
- Alexandre Duret-Lutz (LRDE, EPITA)
We present a collection of command-line tools designed to generate,
filter, convert, simplify, lists of Linear-time Temporal Logic
formulas. These tools were introduced in the release 1.0 of Spot, and
we believe they should be of interest to anybody who has to manipulate
LTL formulas. We focus on two tools in particular: ltlfilt, to filter
and transform formulas, and ltlcross to cross-check
LTL-to-Büchi-Automata translators.
http://publis.lrde.epita.fr/201310-ATVAa
--
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 29 mai 2013 (10--12h), Salle L-Alpha du LRDE.
Au programme:
* 10h: Langages de développement et sécurité --- Mind your language
-- Eric Jaeger et Olivier Levillain, ANSSI (Agence nationale de la sécurité des
systèmes d'information)
http://www.ssi.gouv.fr/fr/anssi/publications/publications-scientifiques/aut…
Il existe de nombreux langages informatiques, et les débats concernant
leurs avantages et inconvénients respectifs sont nombreux, mais peu
considèrent la question du développement d'applications sécurisées,
c'est-à-dire robustes contre les actions d'agents malveillants. C'est
l'optique abordée dans cette présentation, qui rebondit sur de
nombreuses illustrations dans différents langages afin de pouvoir cerner
ce que seraient les bonnes propriétés d'un langage vis-à-vis de la
sécurité, mais aussi des recommandations de codage pertinentes ou encore
des outils pertinents pour le développement et l'évaluation
d'applications de sécurité.
-- Eric Jaeger travaille à l'ANSSI depuis 2004. Après plusieurs années
dans les laboratoires, pendant lesquelles il a notamment travaillé sur
les apports et les limites des méthodes formelles pour les
développements de sécurité, il est devenu chef du centre de formation à
la sécurité des systèmes d'information (CFSSI). Il est à l'origine des
études sur les langages commandées par l'ANSSI depuis 2008 (JavaSec sur
le langage Java, et LaFoSec sur les langages fonctionnels).
-- Olivier Levillain travaille dans les laboratoires de l'ANSSI depuis
septembre 2007 et est aujourd'hui responsable du laboratoire sécurité
des réseaux et protocoles. Il a été l'un des promoteurs et a participé
au suivi des études JavaSec et LaFoSec entre 2008 et 2012. Il prépare
également une thèse sur la sécurité des navigateurs web, se consacrant
pour l'instant essentiellement aux protocoles SSL/TLS.
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.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
http://lists.lrde.epita.fr/listinfo/seminaire
Hello,
I am pleased to announce that I will be giving a talk at the next ECOOP
workshop on Domain Specific Languages Design and Implementation (DSLDI),
to be held in Montpellier, on July 1st 2013.
The abstract is given below:
Language extensibility and its impact on DSL design and implementation:
A case study in Lisp
Out of a concern for focus and concision, domain-specific languages
(DSLs) are usually very different from general purpose programming
languages (GPLs), both at the syntactic and the semantic levels. One
approach to DSL implementation is to write a full language infrastruc-
ture, including parser, interpreter, or even compiler. Another approach
however, is to ground the DSL into an extensible GPL, giving you control
over its own syntax and semantics. The DSL may then be designed merely
as an extension to the original GPL, and its implementation may boil
down to expressing only the differences with it. The task of DSL
implementation is hence considerably eased. The purpose of this talk is
to provide a tour of the features that make a GPL extensible, and to
demonstrate how, in this context, the distinction between DSL and GPL
can blur, sometimes to the point of complete disappearance.
--
ELS 2013, June 3/4, Madrid, Spain: http://els2013.european-lisp-symposium.org
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
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 22 mai 2013 (11--12h), Salle Lα du LRDE.
Au programme:
* 11h: Étendre le compilateur GCC avec MELT
-- Basile Starynkevitch (CEA LIST)
http://gcc-melt.org/
Le compilateur GCC est extensible via des greffons (plugins) depuis
plusieurs années. Mais c'est un logiciel libre complexe (de 10MLOC) et
encore en évolution, dont on décrira grossièrement l'architecture.
Écrire des greffons en C est fastidieux.
Le language d'extension MELT (domain specific language) permet d'étendre
moins péniblemenet le compilateur GCC. Il offre une syntaxe régulière et
simple, inspirée de LISP. MELT est traduit en du code C (ou C++) adapté
aux internes de GCC et son implémentation (en logiciel libre) est
auto-amorcée. Il offre des traits permettant des styles de programmation
de haut niveau (styles fonctionnel, objet, réflexif).
On décrira un peu l'implémentation de MELT, sa syntaxe et ses traits
caractéristiques, et les exemples d'extensions.
-- Basile Starynkevitch est un ancien élève de l'ENS Cachan qui a soutenu
sa thèse en intelligence artificielle en 1990. Il travaille comme
ingénieur chercheur au CEA LIST dans le Laboratoire de Sûreté du
Logiciel, et contribue à GCC en y développant notamment l'outil MELT. Il
est un partisan convaincu du logiciel libre.
!!! Attention !!!
La semaine suivante, le Mercredi 29 mai 2013, changement d'horaire :
nous invitons Eric Jaeger et Olivier Levillain (ANSSI) à 10h-12h pour nous parler
des "Langages de développement et sécurité --- Mind your language".
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.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
_______________________________________________
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 18th International Conference on Implementation
and Application of Automata (CIAA'13) that will take place in Saint
Mary's University, Halifax, Nova Scotia, Canada, on July 16-19, 2013.
Implementation Concepts in Vaucanson 2
Akim Demaille (1), Alexandre Duret-Lutz (1), Sylvain Lombardy (2),
and Jacques Sakarovitch (3)
(1) LRDE, EPITA
(2) LaBRI, Université de Bordeaux
(3) LTCI, CNRS / Télécom-ParisTech
http://publis.lrde.epita.fr/201307-CIAA
Vaucanson is an open source C++ platform dedicated to the computation
with finite weighted automata. It is generic: it allows to write
algorithms that apply on a wide set of mathematical objects. Initiated
ten years ago, several shortcomings were discovered along the years,
especially problems related to code complexity and obfuscation as well
as performance issues. This paper presents the concepts underlying
Vaucanson 2, a complete rewrite of the platform that addresses these
issues.
We are happy to announce that the following paper has been accepted
for publication at the 20th International SPIN Symposium on Model
Checking of Software (SPIN'13) that will take place in Stony Brook,
NY, USA on 8-9 July 2013.
Compositional Approach to Suspension and
Other Improvements to LTL Translation
Tomáš Babiak (1), Thomas Badie (2), Alexandre Duret-Lutz (2),
Mojmír Křetínský (1), and Jan Strejček (1)
(1) Faculty of Informatics, Masaryk University, Brno, Czech Republic
(2) LRDE, EPITA, Kremlin-Bicêtre, France
http://publis.lrde.epita.fr/201307-Spin
Recently, there was defined a fragment of LTL (containing fairness
properties among other interesting formulae) whose validity over a
given infinite word depends only on an arbitrary suffix of the
word. Building upon an existing translation from LTL to Büchi
automata, we introduce a compositional approach where subformulae of
this fragment are translated separately from the rest of an input
formula and the produced automata are composed in a way that the
subformulae are checked only in relevant accepting strongly connected
components of the final automaton. Further, we suggest improvements
over some procedures commonly applied to generalized Büchi automata,
namely over generalized acceptance simplification and over
degeneralization. Finally we show how existing simulation-based
reductions can be implemented in a signature-based framework in a way
that improves the determinism of the automaton.
--
Alexandre Duret-Lutz
We are pleased to announce the release of Spot 1.1.
Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.
This release features several improvements developped with our
collegues from the Mazaryk University (also authors of the ltl3ba
translator) as detailed in the following paper:
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír
Křetínský, Jan Strejček: Compositional Approach to Suspension and
Other Improvements to LTL Translation. To appear in the
proceedings of SPIN'13.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.1.tar.gz
A summary of the changes follows. Please report any issue
to <spot(a)lrde.epita.fr>.
New in spot 1.1 (2013-04-28):
* New features in the library:
- The postprocessor class now takes an optional option_map
argument that can be used to specify fine-tuning options, making
it easier to benchmark different scenarios while developing new
postprocessings.
- A new translator class implements a complete translation chain,
from LTL/PSL to TGBA/BA/Monitor. It performs pre- and
post-processings in addition to the core translation, and offers
an interface similar to that used in the postprocessor class, to
specify the intent of the translation.
- The degeneralization algorithm has learned three new tricks:
level reset, level caching, and SCC-based ordering. The former
two are enabled by default. Benchmarking has shown that the
latter one does not always have a positive effect, so it is
disabled by default. (See SPIN'13 paper.)
- The scc_filter() function, which removes dead SCCs and also
simplify acceptance conditions, has learnt how to simplify
acceptance conditions in a few tricky situations that were not
simplified previously. (See SPIN'13 paper.)
- An experimental "don't care" (direct) simulation has been
implemented. This simulations consider the acceptance
of out-of-SCC transitions as "don't care". It is not
enabled by default because it currently is very slow.
- remove_x() is a function that take a formula, and rewrite it
without the X operator. The rewriting is only correct for
stutter-insensitive LTL formulas (See K. Etessami's paper in IFP
vol. 75(6). 2000) This algorithm is accessible from the
command-line using ltlfilt's --remove-x option.
- is_stutter_insensitive() takes any LTL formula, and check
whether it is stutter-insensitive. This algorithm is accessible
from the command-line using ltlfilt's --stutter-insensitive
option.
- A new translation, called compsusp(), for "Compositional
Suspension" is implemented on top of ltl_to_tgba_fm().
(See SPIN'13 paper.)
- Some experimental LTL rewriting rules that trie to gather
suspendable formulas are implemented and can be activated
with the favor_event_univ option of ltl_simplifier. As
always please check doc/tl/tl.tex for the list of rules.
- Several functions have been introduced to check the
strength of an SCC.
is_inherently_weak_scc()
is_weak_scc()
is_syntactic_weak_scc()
is_complete_scc()
is_terminal_scc()
is_syntactic_terminal_scc()
Beware that the costly is_weak_scc() function introduced in Spot
1.0, which is based on a cycle enumeration, has been renammed to
is_inherently_weak_scc() to match established vocabulary.
* Command-line tools:
- ltl2tgba and ltl2tgta now honor a new --extra-options (or -x)
flag to fine-tune the algorithms used. The available options
are documented in the spot-x (7) manpage. For instance use '-x
comp-susp' to use the afore-mentioned compositional suspension.
- The output format of 'ltlcross --json' has been changed slightly.
In a future version we will offer some reporting script that turn
such JSON output into various tables and graphs, and these change
are required to make the format usable for other benchmarks (not
just ltlcross).
- ltlcross will now count the number of non-accepting, terminal,
weak, and strong SCCs, as well as the number of terminal, weak,
and strong automata produced by each tool.
* Documentation:
- org-mode files used to generate the documentation about
command-line tools (shown at http://spot.lip6.fr/userdoc/tools.html)
is distributed in doc/org/. The resulting html files are also
in doc/userdoc/.
* Bug fixes:
- There was a memory leak in the LTL simplification code, that could
only be triggered when disabling advanced simplifications.
- The translation of the PSL formula !{xxx} was incorrect when xxx
simplified to false.
- Various warnings triggered by new compilers.
--
Alexandre Duret-Lutz