- Annonce

New publication: Quotient Operators for Weighted Rational Expressions
by Akim Demaille 06 Jul '17

06 Jul '17

The Vcsn team is happy to announce that the following paper was accepted to the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017), to be held in 23-27 October 2017 in Hanoi, Vietnam. Quotient Operators for Weighted Rational Expressions Akim Demaille, Thibaud Michaud EPITA/LRDE Quotients of words play a key role in formal language theory, however they have been rarely studied in the context of weighted rational expressions. We define the left and right quotients of rational series, and introduce corresponding operators for weighted expressions. We generalize an alternative construction of the derived-term (or Antimirov, or equation) automaton, based on expansions, to handle these operators. For more information about this publication see http://publis.lrde.epita.fr/demaille.17.ictac To visit Vcsn's home page, go to (considered harmless) http://vcsn.lrde.epita.fr To play with Vcsn on the topic of this paper http://vcsn-sandbox.lrde.epita.fr/notebooks/Doc/ICTAC-2017.ipynb

1 0

L'air de rien 38.0
by Daniela Becker 30 Jun '17

30 Jun '17

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°38 du bulletin du LRDE. C'est un numéro spécial dédié aux séminaires des étudiants-chercheurs du LRDE qui auront lieu le mardi 4 juillet 2017. Vous y trouverez le programme de la journée avec les résumés des exposés. Nous y laissons également la parole à trois de nos collègues qui ont décidé de partir pour de nouveaux horizons. Vous pouvez télécharger le bulletin en couleur à la page suivante : http://www.lrde.epita.fr/wiki/LrdeBulletin/l-air-de-rien-38 -- Daniela Becker Responsable administrative du LRDE

1 0

Publication accepted at SAT'2017
by Souheib Baarir 30 Jun '17

30 Jun '17

I am happy to announce that the following paper has been accepted at the 20th International Conference on Theory and Applications of Satisfiability Testing to be held in Melbourne, Australia from August 28th to September 1st. "PaInleSS: a Framework for Parallel SAT Solving" Ludovic Le Frioux (1,2), Souheib Baarir (1,2,3), Julien Sopena (2), and Fabrice Kordon (2) (1) LRDE, EPITA, Kremlin-Bicêtre, France (2) Sorbonne Universites, UPMC Univ Paris 06, UMR 7606, LIP6, Paris, France CNRS, UMR 7606, LIP6, Paris, France (3) Universite Paris Nanterre, France. Abstract : Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programming, involved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool. We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers. Souheib Baarir.

1 0

[Séminaire des étudiants CSI] Mardi 4 juillet 2017 - Salle L0
by Daniela Becker 21 Jun '17

21 Jun '17

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mardi 4 juillet 2017 à partir de 10h00 en L0 au LRDE (KB). -------------------------------------------- Au programme : SPOT — BIBLIOTHÈQUE DE MODEL CHECKING 10h00 : Un ensemble d’outils de conversion en automate de co-Büchi – ALEXANDRE GBAGUIDI AÏSSE Spot supporte des conditions d’acceptation arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversion capables de convertir (quand c’est possible) n’importe quel automate avec une condition d’acceptation classique vers du co-Büchi déterministe. Nous présenterons ces algorithmes mis au point par Boker et Kupferman en explicitant les améliorations apportées durant leur implémentation. 10h30 : Test de vacuité bi-bande dans Spot – CLÉMENT GILLARD Lorsqu’on fait de la vérification de modèle à l’aide d’ω- automates, une opération typique est le calcul de L(AxB) ≠ Ø. Son implémentation par empty(product(A,B)) pose problème, car le produit utilise autant d’ensembles d’acception qu’il y en a dans A et dans B et ce nombre d’ensembles ne peut excéder 32 dans Spot. On propose empty(A,B) qui ne construit pas d’automate et retire cette contrainte sur les automates en entrée. 11h00 : Réduction par simulation à n pas – LAURENT XU En vérification formelle à l’aide d’ω-automates, il est utile de réduire la taille des automates. L. Clemente et R. Mayr présentent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l’augmentation de ce nombre de pas améliore la réduction. Nous étudions une généralisation de la réduction d’ω- automates par simulation reposant sur la signature des états à un pas de Spot afin qu’elle fonctionne également à n pas. 11h30 : Réduction d’ordre partiel dans SPOT – VINCENT TOURNEUR Les outils de vérification formelle souffrent actuellement d’un problème de passage à l’échelle. La réduction d’ordre partiel (POR) est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Nous allons parler de l’implémentation de certains de ces algorithmes de POR dans la bibliothèque Spot, puis de leur optimisation. 13h30 : Intégration de TChecker dans Spot – ARTHUR REMAUD Les automates temporisés sont un type d'ω-automate représentant des modèles comportant des conditions de temps continu. Spot ne gère actuellement pas ce type d’automates. TChecker est un outil développé par le LaBRI travaillant sur des automates temporisés. Plutôt que réimplémenter tous les algorithmes, TChecker a été intégré dans Spot via un nouvel exécutable. 14h00 : Synthèse LTL avec Spot – THIBAUD MICHAUD Nous présentons un nouvel outil de synthèse de circuit à partir de spécifications LTL. Il réduit le problème de synthèse à un jeu à parité, qui est résolu grâce à l’un des deux algorithmes implémentés. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d’origine. OLENA — TRAITEMENT D’IMAGES GÉNÉ- RIQUE ET PERFORMANT 14h45 : L’Arbre de partition binaire pour le traitement d’images – FABIEN HOUANG L’arbre de partition binaire est, en traitement d’images, une structure qui permet la segmentation et la recherche efficace d’information dans une image. Il peut être créé à partir de différents modèles de région et fonctions de calcul de distance entre ces régions. La construction de cet arbre se fait habituellement à partir d’une image pré-segmentée pour des questions de performance. La sensibilité de l’arbre au bruit dans l’image peut aussi être étudiée, pour trouver par exemple quels niveaux de l’arbre sont influencés par ce dernier. 15h15 : Calcul du Complexe de Morse- Smale à l’aide de coupe de ligne de partage des eaux – VICTOR COLLETTE Le complexe de Morse-Smale est un outil utile pour analyser la topologie d’une image. Son calcul étant onéreux avec un algorithme classique, L. Comic a émis l’hypothèse que son calcul pouvait être réalisé à l’aide d’un algorithme de coupe de ligne de partage des eaux. Nous parlerons donc de cette possibilité et des différents problèmes que cette solution engendre. 15h45 : Méthode d’évaluation d’évaluateur d’algorithme de détection de texte – ALIONA DANGLA Plusieurs méthodes d’évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents. Afin d’évaluer ces méthodes, la solution proposée est de confronter les évaluations automatiques avec l’évaluation humaine en considérant celle-ci comme référence. Pour l’obtenir, un site internet à été réalisé afin d’obtenir un classement cohérent. -- Daniela Becker Responsable administrative du LRDE

1 0

Olivier Ricou participe à PyParis 2017
by Daniela Becker 08 Jun '17

08 Jun '17

Bonjour, nous avons le plaisir de vous annoncer qu'Olivier Ricou, directeur du LRDE, est invité à participer dans le cadre de la Conférence PyParis 2017 (http://www.pyparis.org) à une table ronde le mardi 13 juin 2017. Il y fera un retour d’expérience sur la création d'un MOOC Python pour les scientifiques. -- Daniela Becker Responsable administrative - LRDE

1 0

[Seminaire-LRDE] Séminaire du LRDE le mercredi 14 juin 2017: Andrés S. Charif Rubial (ESN PeXL et Li-PARAD - Université de Versailles)
by Guillaume Tochon 31 May '17

31 May '17

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 14 juin 2017 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-06-14 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 14 juin 2017 : * 11h--12h: MAQAO: une suite d'outils pour l'analyse et l’optimisation des performances -- Andrés S. Charif Rubial (ESN PeXL et Li-PARAD - Université de Versailles) www.maqao.org MAQAO (Modular Assembly Quality Analyzer and Optimizer) est une suite d'outils d'analyse et d'optimisation des performances à destination d'applications binaires. Le but principal de MAQAO est d'analyser des codes binaires puis de proposer aux développeurs d'applications des rapports synthétiques les aidant à comprendre et optimiser les performances de leur application. MAQAO combine des analyses statiques (évaluation de la qualité du code) et dynamiques (profiling) basées sur la capacité à reconstruire des structures aussi bien bas niveau (basic blocks, instructions, etc.) que haut niveau (fonctions et boucles). Un autre aspect important de MAQAO est son extensibilité. En effet les utilisateurs peuvent écrire leur propre plugin grâce à un langage de script simple intégré (Lua). -- Le Dr. Andres S. CHARIF RUBIAL dirige aujourd'hui une ESN dont les principales activités sont le HPC, l’ingénierie système, réseau et sécurité. En parallèle il est chercheur hébergé au Laboratoire Li-PARAD de l'Université de Versailles. Il a dirigé pendant 4 ans l'équipe de recherche et développement "évaluation des performance" du laboratoire Exascale Computing Research Laboratory (situé sur le campus Teratec). Il a principalement supervisé et travaillé au développement de la suite d'outils MAQAO afin de mieux comprendre les problèmes de performance des applications HPC mono et multi-noeuds. Ses travaux de thèse achevés en 2012 portaient d'ailleurs déjà sur cette thématique, en particulier sur le profilage d'applications et les problématiques de caractérisation des performances mémoire sur des systèmes à mémoire partagée. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

Interspeech 2017 Notification of Acceptance
by Réda Dehak 23 May '17

23 May '17

> Début du message réexpédié : > > The peer review process for Interspeech 2017 is now completed. Each and every paper has received at least 3 reviews, and the Technical Program Committee has thoroughly analyzed the scores and comments of the reviewers to put together an exciting technical program for the conference. Given the large number of high-quality submissions received, this has proved to be a difficult task, and many interesting papers could not be included. This year the overall acceptance rate is about 50%. > > We are pleased to inform you that your paper: > > Paper ID: 537 > Title: The MIT-LL, JHU and LRDE NIST 2016 Speaker Recognition > Evaluation System > > has been selected for a presentation at the conference.

1 0

New publication: Explicit State Model Checking with Generalized Büchi and Rabin Automata
by Alexandre Duret-Lutz 22 May '17

22 May '17

I'm happy to announce that the following article has been accepted for publication in the International SPIN Symposium on Model Checking of Software (SPIN'17), to be held in Santa Barbara on July 13-14, 2017. « Explicit State Model Checking with Generalized Büchi and Rabin Automata » Vincent Bloemen¹ Alexandre Duret-Lutz² Jaco van de Pol¹ ¹ University of Twente, Enschede, The Netherlands ² LRDE / EPITA, Le Kremlin-Bicêtre, France Abstract: In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure. This paper investigates whether using a more general form of acceptance, namely transition-based generalized Rabin automata (TGRAs), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice. We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly. http://www.lrde.epita.fr/dload/papers/bloemen.17.spin.pdf -- Alexandre Duret-Lutz

1 0

[Seminaire-LRDE] Séminaire du LRDE le mercredi 3 mai 2017: Pierre Sermanet, Google Brain
by Guillaume Tochon 25 Apr '17

25 Apr '17

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 3 mai 2017 (11h--12h), Amphi 3 de l'EPITA. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-05-03 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 3 mai 2017 : * 11h--12h: Apprentissage par Imitation Auto-Supervisée -- Pierre Sermanet, Google Brain https://sermanet.github.io/tcn/ Nous proposons une approche auto-supervisée pour l’apprentissage de représentations à partir de vidéos non supervisées, enregistrées à de multiples points de vue. Cette approche est particulièrement pertinente en robotique pour l’apprentissage par l’imitation, qui nécessite une compréhension invariante par rapport au point de vue des relations entre les humains et leur environnement (telles que les interactions entre objets, les attributs et les poses corporelles). Nous entraînons nos représentations à l’aide d’une stratégie de type triplet loss, où les multiples points de vue simultanés de la même observation sont attirés dans l’espace d’intégration, tout en étant repoussés des voisins temporels qui sont souvent visuellement similaires mais fonctionnellement différents. Ce signal encourage notre modèle à découvrir des attributs invariants vis-à-vis du point de vue, mais qui varient dans le temps, tout en ignorant les potentielles nuisances telles que les occlusions, le flou de mouvement, l’éclairage et l’arrière-plan. Nos expériences démontrent qu’une telle représentation acquiert même un certain degré d’invariance vis-à-vis de l’instance d’objet. Nous montrons que notre modèle peut correctement identifier les étapes correspondantes dans les interactions complexes d’objets, à travers différentes vidéos avec différentes instances. Nous montrons également les premiers résultats, à notre connaissance, d’apprentissage intégralement auto-supervisé pour l’imitation de mouvements humains par un robot réel. -- Pierre Sermanet est issu de la promo EPITA 2005 (spécialisation GISTR). En 2004 il participe avec Evolutek à la compétition robotique Eurobot <http://cs.nyu.edu/~sermanet/eurobot.html>. Après son stage de fin d’étude chez Siemens Research à Princeton, il travaille avec Yann LeCun en tant qu’ingénieur de recherche pendant 3 ans sur le thème du deep learning pour le projet de robotique mobile LAGR <http://cs.nyu.edu/~sermanet/lagr.html>. Il effectue ensuite son doctorat en deep learning avec Yann LeCun à l'Université de New York jusqu’en 2013, puis il rejoint ensuite Google Brain en tant que chercheur en deep learning appliqué à la vision et à la robotique. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

publication: Seminator: A Tool for Semi-Determinization of Omega-Automata
by Alexandre Duret-Lutz 03 Apr '17

03 Apr '17

I am happy to announce that the following paper has been accepted at the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21) to be held in Maun, Botswana, on 7-12th May 2017. Seminator: A Tool for Semi-Determinization of Omega-Automata František Blahoudek¹, Alexandre Duret-Lutz², Mikuláš Klokočka¹, Mojmír Křetínský¹, Jan Strejček¹ ¹Faculty of Informatics, Masaryk University, Brno, Czech Republic ²LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/blahoudek.17.lpar Abstract: We present a tool that transforms nondeterministic ω-automata to semi-deterministic ω-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation. -- Alexandre Duret-Lutz

1 0