I am happy to announce that the following paper has just been
published in Vol. 5 of the International Journal on Critical
Computer-based Systems:
LTL Translation Improvements in Spot 1.0
Alexandre Duret-Lutz (LRDE/EPITA)
This is an extended version of my VECOS'11 paper, that was submitted
to IJCCBS in October 2012, accepted in April 2013, and published in
March 2014.
https://www.lrde.epita.fr/wiki/Publications/duret.14.ijccbs
Abstract:
Spot is a library of model-checking algorithms started in 2003.
This paper focuses on its module for translating linear-time
temporal logic (LTL) formulas into Büchi automata: one of the
steps required in the automata-theoretic approach to LTL
model-checking.
We detail the different algorithms involved in this translation: the
core translation itself, which performs many simplifications thanks
to its use of binary decision diagrams; the pre-processing of the LTL
formulas with rewriting rules chosen to help their translation;
and various post-processing algorithms whose use depends on the
intent of the translation: do we favor deterministic automata, or
small automata?
Using different benchmarks, we show how Spot competes with other
LTL translators, and how it has improved over the years.
--
Alexandre Duret-Lutz
Bonjour,
nous avons le plaisir de vous annoncer que le Laboratoire de Recherche
et Développement de l'EPITA (LRDE) a été retenu pour le programme de recherche
bilatéral franco-tchèque PHC Barrande 2014.
Ce programme a pour objectif de favoriser les échanges scientifiques et
technologiques entre des laboratoires de recherche des deux pays.
Le financement accordé pour le LRDE permettra de réaliser des actions de mobilité
de jeunes chercheurs, de doctorants et post-doctorants dans le cadre du projet Spot
avec le partenaire tchèque, la Faculté d'Informatique de la Masaryk University à Brno.
Pour en savoir plus : http://www.campusfrance.org/fr/barrande
--
Daniela Becker
Responsable administrative - LRDE
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 12 mars 2014 (11h--12h30), Salle L0 du LRDE.
Au programme:
* 11h-12h30: Programmation d'applications Web client-serveur avec Ocsigen
-- Vincent Balat, Université Paris Diderot et INRIA
http://ocsigen.org
Le Web a subi en quelques années une évolution radicale, passant d'une
plateforme de données à une plateforme d'applications. Mais la plupart
des outils de programmation n'ont pas été conçus pour cette nouvelle
vision du Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de
programmation adaptées aux besoins des sites Web modernes et des
applications Web distribuées. Il permet de programmer les parties client
et serveur dans le même langage, et même, comme une seule et même
application. La puissance expressive du langage OCaml permet
d'introduire une abstraction des technologies sous-jacentes dans le but
de simplifier la programmation d'interactions Web complexes. Le système
de types très avancé du langage permet d'améliorer la fiabilité des
programmes et le respect des standards. Cela permet aussi de réduire
beaucoup le temps de développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire
un exemple d'application simple.
-- Vincent Balat est maître de conférences à l'université Paris Diderot,
actuellement en délégation à l'INRIA. Il est le créateur et chef du
projet Ocsigen. Il est ancien élève de l'École Normale Supérieure de
Cachan. Son travail de recherche porte essentiellement sur
l'amélioration de l'expressivité et de la fiabilité des techniques de
programmation Web.
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://lists.lrde.epita.fr/listinfo/seminaire
Bonjour,
nous avons le plaisir de vous annoncer que le Laboratoire de Recherche
et Développement de l'EPITA (LRDE) intègre l'EDITE de Paris, école doctorale
informatique, télécommunications et électronique. Le LRDE pourra désormais
encadrer des bourses CIFRE.
--
Daniela Becker
Responsable administrative - LRDE
(Laboratoire de Recherche et Développement de l'Epita)
Tél: +33 1 53 14 59 22 -- Fax: +33 1 53 14 59 13
Daniela.Becker(a)lrde.epita.fr
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
Mardi 18 février 2014 (18h20--19h30), Amphi 4.
Au programme:
* 18h20: CLAIRE : un pseudo-code élégant exécutable et compilable pour l'aide à la décision
-- Yves Caseau, Bouygues Telecom & Académie des Technologies
http://claire3.free.fr/
CLAIRE est un langage créé il y a une vingtaine d'années pour
développer, partager et enseigner des algorithmes pour la recherche
opérationnelle. Notre ambition première était de créer un pseudo-code
exécutable, qui permette à la fois de décrire simplement des algorithmes
complexes et de les exécuter facilement, grâce à un interprète, et
rapidement, grâce à un compilateur.
Après avoir brièvement rappelé l'histoire et les motivations de ce
projet, la deuxième partie de l'exposé donnera des exemples de fragments
de code, ainsi que quelques exemples d'applications réussies qui donnent
un peu de crédit à cette ambition.
La troisième partie fera un zoom sur certaines propriétés originales de
CLAIRE, qui font que ce langage de programmation conserve un certain
intérêt dans le paysage de 2014. En particulier, CLAIRE permet de
décrire des algorithmes d'exploration arborescents avec des mécanismes
natifs de raisonnement hypothétique. Un autre intérêt de ce langage est
le haut niveau de polymorphisme paramétrique, qui permet de traiter des
fragments de code comme des structures de données. CLAIRE a été utilisé
pour développer différents outils d'aide à la décision, de la résolution
de problèmes d'optimisation combinatoire à la simulation, en particulier
dans le cadre de GTES (simulation par jeux et apprentissage).
La dernière partie de cet exposé fera la liste des ressources
disponibles pour répondre à la question: pourquoi s'intéresser à un
langage désuet ``20 ans après'' ? Le code de CLAIRE ---
méta-description, interprète et plate-forme de compilation --- est
disponible. Une partie des fragments de code disponibles peuvent soit
servir de source d'inspiration (lorsqu'il s'agit de fonctionnalités qui
restent originales) soit de code réutilisable.
-- Yves Caseau est directeur général adjoint Technologie, Prospectives et
Innovation à Bouygues Telecom dont il a été le DSI de 2001 à 2006. Il a
commencé sa carrière dans la recherche, à Telcordia (USA) puis à la tête
du e-Lab de Bouygues. Il est passé de l'intelligence artificielle à la
programmation par contraintes, puis à la recherche opérationnelle pour
terminer plus récemment par la simulation et la théorie des jeux.
-- Ancien élève de l'ENS Ulm, il est également titulaire d'un MBA du
Collège des ingénieurs, ainsi que d'un doctorat en informatique (Paris
XI) et d'une habilitation à diriger des recherches (Paris VII). Il est
membre de l'Académie des Technologies et auteur de trois livres publiés
chez Dunod.
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://lists.lrde.epita.fr/listinfo/seminaire
ELS'14 - 7th European Lisp Symposium
IRCAM, Paris, France
May 5-6, 2014
http://www.european-lisp-symposium.org/
Latest News:
* Registration is now open. Early registration fee until April 13.
See http://www.european-lisp-symposium.org/content-registration-full.html
* Submission deadline is approaching. Still one month to submit a paper!
* Thanks to our new sponsors, Lispworks and Franz Inc.!
http://www.lispworks.com/http://franz.com/
The purpose of the European Lisp Symposium is to provide a forum for
the discussion and dissemination of all aspects of design,
implementation and application of any of the Lisp and Lisp-inspired
dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP,
Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We
encourage everyone interested in Lisp to participate.
The 7th European Lisp Symposium invites high quality papers about
novel research results, insights and lessons learned from practical
applications, and educational perspectives. We also encourage
submissions about known ideas as long as they are presented in a new
setting and/or in a highly elegant way.
Topics include but are not limited to:
- Context-, aspect-, domain-oriented and generative programming
- Macro-, reflective-, meta- and/or rule-based development approaches
- Language design and implementation
- Language integration, inter-operation and deployment
- Development methodologies, support and environments
- Educational approaches and perspectives
- Experience reports and case studies
Please note that IRCAM, the conference venue, is a French institute
for research on music and acoustics. Submissions relating Lisp to
music or other acoustical matters will hence be particularly welcome,
although given no heightened favor during the review process.
We invite submissions in the following forms:
Papers: Technical papers of up to 8 pages that describe original
results or explain known ideas in new and elegant ways.
Demonstrations: Abstracts of up to 2 pages for demonstrations of
tools, libraries, and applications.
Tutorials: Abstracts of up to 4 pages for in-depth presentations about
topics of special interest for at least 90 minutes and up to 180
minutes.
The symposium will also provide slots for lightning talks, to be
registered on-site every day.
All submissions should be formatted following the ACM SIGS guidelines
and include ACM classification categories and terms. For more
information on the submission guidelines and the ACM keywords, see:
http://www.acm.org/sigs/publications/proceedings-templates and
http://www.acm.org/about/class/1998.
Important dates:
- TODAY: Mark your calendar. Start planning now!
- 09 Mar 2014: Submission deadline
- 31 Mar 2014: Notification of acceptance
- 13 Apr 2014: Early registration deadline
- 21 Apr 2014: Final Papers due
- 05 May 2014: Symposium. Join us there!
Programme chair:
Kent Pitman, Hypermeta Inc., U.S.A.
Local chairs:
Didier Verna, EPITA Research Lab, France
Gérard Assayag, IRCAM, Paris, France
Programme committee:
To be announced later
Local organizers:
Daniela Becker, EPITA Research Lab, France
Sylvie Benoit, IRCAM, Paris, France
Search Keywords:
#els2014, ELS 2014, ELS '14, European Lisp Symposium 2014,
European Lisp Symposium '14, 7th ELS, 7th European Lisp Symposium,
European Lisp Conference 2014, European Lisp Conference '14
Ircam STMS Lab, IRCAM / CNRS / UPMC
--
Please help crowdfund my next Jazz quartet album !!
http://www.kisskissbankbank.com/quartet-the-second-album
Lisp, Jazz, Aïkido: http://www.didierverna.info
Bonjour,
le séminaire de Vincent Balat, Université Paris Diderot et INRIA,
prévu le mercredi 5 février est reporté au mercredi 12 mars.
Mais veuillez d'ores et déjà retenir la date du mercredi 12 février 2014,
11h--12h30, Salle L0 du LRDE : nous acceillons Dominique Revuz,
LIGM, UMR 8046, Université Paris-Est Marne-la-Vallée avec un exposé
sur les "Automates Acycliques".
Au programme:
* 11h: Automates Acycliques
-- Dominique Revuz, LIGM, UMR 8046, Université Paris-Est Marne-la-Vallée
http://astl.sourceforge.net/
Les automates acycliques sont utilisés dans tous les logiciels de
traitement de la langue naturelle essentiellement pour la représentation
des lexiques, des dictionnaires et des interprétations
morpho-syntaxiques des textes.
Nous présenterons des résultats sur les stratégies de construction, de
manipulation et de stockage de ces automates. En particulier un
alogrithme de construction dynamique.
-- Docteur de l'Université Paris 7. Directeur de l'ESIPE, école
d'ingénieurs de l'université de Marne-la-Vallée. Spécialisé en
compression et représentation de données en mémoire.
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://lists.lrde.epita.fr/listinfo/seminaire
Chers collègues,
Le mois de février 2014 sera riche en interventions à l'occasion
du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA),
car nous organisons trois séminaires :
* Le mercredi 5 février 2014, 11h--12h30, Salle L0 du LRDE,
nous accueillons Vincent Balat, Université Paris Diderot et INRIA,
pour nous parler de la "Programmation d'applications Web
client-serveur avec Ocsigen".
* Le mercredi 12 février 2014, 11h--12h30, Salle L0 du LRDE,
nous invitons Dominique Revuz, LIGM, UMR 8046, Université Paris-Est
Marne-la-Vallée avec un exposé sur les "Automates Acycliques".
* Attention changement de jour, d'horaire et de lieu !!
Le mardi 18 février 2014,18h20--19h30, Amphi 4 EPITA-KB,
nous avons le plaisir de recevoir Yves Caseau, Bouygues Telecom & Académie
des Technologies pour un exposé intitulé "CLAIRE : un pseudo-code élégant
exécutable et compilable pour l'aide à la décision".
Au programme du Mercredi 5 février 2014 :
* 11h-12h30: Programmation d'applications Web client-serveur avec Ocsigen
-- Vincent Balat, Université Paris Diderot et INRIA
http://ocsigen.org
Le Web a subi en quelques années une évolution radicale, passant d'une
plateforme de données à une plateforme d'applications. Mais la plupart
des outils de programmation n'ont pas été conçus pour cette nouvelle
vision du Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de
programmation adaptées aux besoins des sites Web modernes et des
applications Web distribuées. Il permet de programmer les parties client
et serveur dans le même langage, et même, comme une seule et même
application. La puissance expressive du langage OCaml permet
d'introduire une abstraction des technologies sous-jacentes dans le but
de simplifier la programmation d'interactions Web complexes. Le système
de types très avancé du langage permet d'améliorer la fiabilité des
programmes et le respect des standards. Cela permet aussi de réduire
beaucoup le temps de développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire
un exemple d'application simple.
-- Vincent Balat est maître de conférences à l'université Paris Diderot,
actuellement en délégation à l'INRIA. Il est le créateur et chef du
projet Ocsigen. Il est ancien élève de l'École Normale Supérieure de
Cachan. Son travail de recherche porte essentiellement sur
l'amélioration de l'expressivité et de la fiabilité des techniques de
programmation Web.
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://lists.lrde.epita.fr/listinfo/seminaire
Bonjour,
nous avons le plaisir de vous inviter au séminaire des étudiants-chercheurs du
LRDE. Il aura lieu le mercredi 22 janvier 2014 à partir de 10 heures en
Amphi 1 (KB).
-----------------------------------------------------------------------
Au programme :
* 10h00 : Introduction
OLENA
* 10h15 : Utilisation d’un descripteur à
base de transformée en ondelettes pour
extraire des informations sur la forme
des objets – Raphaël Boissel
* 10h45 : Revue comparative des algorithmes
de calcul de l’arbre des formes – Sébastien Crozet
CLIMB
* 11h30 : Coercition et programmation
orientée contexte – François Ripault
VERIFICATION DU LOCUTEUR
* 12h00 : Prise de décision à l’aide de SVM
dans le contexte des systèmes de vérification
du locuteur à base d’I-Vector – Benjamin Roux
Les Résumés des exposés :
**************************
OLENA
* 10h15 : Utilisation d’un descripteur à
base de transformée en ondelettes pour
extraire des informations sur la forme
des objets – Raphaël Boissel
Le système de localisation de texte développé par le laboratoire
est actuellement en mesure de séparer le texte du fond
dans les images naturelles au moyen d’un descripteur basé sur
la transformée en ondelettes. De plus, les tests montrent que ce
système est rapide et précis pour accomplir cette tâche. Notre
objectif principal est d’extraire de nouvelles informations sur la
forme des objets lors de la phase de classification en utilisant
le même descripteur que celui utilisé pour séparer le texte du
fond. De telles informations peuvent être utilisées pour améliorer
la précision d’autres étapes du système de localisation de
texte. De plus, puisque le descripteur utilisé pour extraire ces
informations a déjà été calculé, cette approche est peu consommatrice
en temps CPU. Par ailleurs, plus que des informations
sur la forme des objets, ce descripteur peut également être utilisé
tel quel pour créer un O.C.R. (Reconnaissance optique de
caractère) simple. Cependant, afin de mettre en place ces changements,
il est nécessaire de retravailler le système de classification
et le système d’apprentissage mis en place précédemment.
Différentes méthodes pour atteindre ces objectifs sont
présentées ici et comparées afin de savoir quelle sorte d’information
il est possible d’extraire à partir du descripteur à base
de transformée en ondelettes.
* 10h45 : Revue comparative des algorithmes
de calcul de l’arbre des formes – Sébastien Crozet
L’arbre des formes est une transformée d’image utile pour les
traitements d’images discrètes de façon auto-duale. Bien qu’il
puisse être calculé grâce à plusieurs approches existantes dans
la littérature, aucune comparaison de ces algorithmes n’a été
réalisée jusqu’à présent. Nous réalisons une comparaison de
tous ces algorithmes du point de vue de leur rapidité de calcul
et de leur occupation mémoire. Nous étudions aussi la parallélisation
de l’algorithme quasi-linéaire et modifions les données
qu’il manipule afin d’améliorer ses temps de calculs et son occupation
mémoire.
CLIMB
* 11h30 : Coercition et programmation
orientée contexte – François Ripault
La programmation orientée contexte est un paradigme prometteur
pour prendre en compte les problématiques transverses
dans le logiciel. Ce paradigme permet de spécialiser les
classes et les méthodes en fonction du contexte. Cependant, il
ne traite pas la coercition, c’est-à-dire la conversion d’un objet
existant dans un certain contexte vers une nouvelle représentation
dans un autre contexte. Nous montrons en quoi ce manque
est critique, en fournissant des exemples extraits de Climb, une
bibliothèque de traitement d’images écrite en Common Lisp.
Nous proposons des solutions pour la coercition automatique
d’objets, et nous les analysons en termes de simplicité et de
généricité.
VERIFICATION DU LOCUTEUR
* 12h00 : Prise de décision à l’aide de SVM
dans le contexte des systèmes de vérification
du locuteur à base d’I-Vector – Benjamin Roux
La prise de décision dans l’état de l’art des systèmes de vérification
du locuteur est basée sur la distance en cosinus. Une
approche différente est de considérer une prise de décision
basée sur les Séparateurs à Vaste Marge (SVM). La technique
des SVM a été largement exploitée dans la reconnaissance de
formes et la prise de décision mais également en association
avec les GMM super-vecteurs (GSV) en reconnaissance du locuteur.
Cependant, l’idée d’utiliser les SVM dans l’espace des
i-vectors pour la reconnaissance du locuteur n’a pas été le sujet
d’une étude approfondie. Nous étudierons les différentes
fonctions kernels et comment cela peut être utilisé dans la vérification
du locuteur. Nous explorerons comment prendre en
compte les variabilités de canal et de locuteur et dans l’espace
des caractéristiques. Nous expérimenterons avec les données
de la base NIST-SRE 2010.
--
Daniela Becker
Responsable administrative - LRDE
We are please at the following paper has been accepted in the 20th
International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS). Please find the title and abstract
below.
Title and corresponding authors:
Symbolic Model Checking of stutter invariant properties Using
Generalized Testing Automata.
A. Ben Salem(1), A. Duret-Lutz(1), F. Kordon(2), and Y. Thierry-Mieg(2)
(1) LRDE-EPITA, www.lrde.epita.fr
(2) UPMC-LIP6, www.lip6.fr
Abstract:
Previous work showed that a kind of omega-automata known as
Transition-based Generalized Testing Automata (TGTA) can outperfrom the
Büchi automata traditionally used for \textit{explicit} model checking
when verifying stutter-invariant properties.
In this work, we investigate the use of these generalized testing
automata to improve \textit{symbolic} model checking of
stutter-invariant LTL properties. We propose an efficient symbolic
encoding of stuttering transitions in the product between a model and a
TGTA. Saturation techniques available for decision diagrams then benefit
from the presence of stuttering self-loops on all states of TGTA.
Experimentation of this approach confirms that it outperforms the
symbolic approach based on (transition-based) Generalized Büchi
Automata.