March 2016 - Annonce

publications: two papers accepted at Spin'15
by Alexandre Duret-Lutz 20 Jun '16

20 Jun '16

I am happy to announce that the following two papers have been accepted at the 22nd International SPIN Symposium on Model Checking of Software (SPIN 2015) to be held in Stellenbosch, South Africa on 24–26 August 2015. --- On Refinement of Büchi Automata for Explicit Model Checking František Blahoudek¹, Alexandre Duret-Lutz², Vojtěch Rujbr¹, and 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.15.spin Abstract: In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand andmore importantly, for which the explicit model checking process performs better. --- Practical Stutter-Invariance Checks for ω-Regular Languages Thibaud Michaud and Alexandre Duret-Lutz LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/michaud.15.spin Abstract: We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns out, implementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant. -- Alexandre Duret-Lutz

3 2

Article accepted to European Lisp Conference 2016
by Jim Newton 30 Mar '16

30 Mar '16

We are happy to announce that our paper entitled Type-Checking of Heterogeneous Sequences in Common Lisp authored by Jim Newton, Akim Demaille, and Didier Verna has been accepted for presentation and publication at the 9th European Lisp Symposium (http://www.european-lisp-symposium.org) Abstract: We introduce the abstract concept of rational type expression and show its relationship to rational language theory. We further present a concrete syntax, regular type expression, and a Common Lisp implementation thereof which allows the programmer to declaratively express the types of heterogeneous sequences in a way which is natural in the Common Lisp language. The implementation uses techniques well known and well founded in rational language theory, in particular the use of the Brzozowski derivative and deterministic automata to arrive at a solution which can match a sequence in linear time. We illustrate the concept with several motivating examples, and finally explain many details of its implementation. Please find the link to the article and a longer more elaborate project report here: https://www.lrde.epita.fr/wiki/Publications/newton.16.els.inc If you have any questions or comments about the paper, we are happy to discuss them with you. Jim

1 0

Prochain séminaire MeFoSyLoMa : vendredi 8 avril 2016 au LRDE (Epita)
by Alexandre Duret-Lutz 30 Mar '16

30 Mar '16

Bonjour à tous, La prochaine séance du séminaire MeFoSyLoMa sera orientée outils, et se tiendra au LRDE. ======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/ Méthodes Formelles pour Les Systèmes Logiciels et Matériels Vendredi 8 avril 2016, 14h-17h Adresse: LRDE (Epita), Salle Alpha Bâtiment X, 2e étage 18 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : https://www.google.com/maps?q=48.8152808,2.3623765 https://www.lrde.epita.fr/~adl/dl/acces-lrde.pdf S'il y en a parmi vous qui comptent venir en voiture, le parking du centre commercial Okabé est gratuit pendant 3h. http://www.okabe.com/okabe/fr/okabe-parking ======================================================================== Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC), LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la confrontation de différentes approches ou points de vue sur l'utilisation des méthodes formelles dans les domaines du génie logiciel, de la conception de circuit, des systèmes répartis, des systèmes temps-réel ou encore des systèmes d'information. Il s'organise autour de réunions bimestrielles où sont exposés des travaux de recherche récents sur ce thème. ======================================================================== Programme 14h00-14h45: Alexandre Duret-Lutz (LRDE/Epita) Spot 2.0 Je présenterai Spot 2.0, une bibliothèque C++ de manipulation d'omega-automates pour le model checking. Les nouveautés sont assez nombreuses: la bibliothèque travaille maintenant avec des automates dont la condition d'acceptation peut être arbitrairement complexe (par exemple une combinaison booléenne de Streett et Rabin généralisé), de nouveaux outils en ligne de commande permettent de manipuler et produire ces automates, et la majeur partie des fonctionnalités est utilisable avec une surcouche de bindings pour Python. Je montrerai en particulier: - des exemples d'utilisation tirés du cours d'initiation au model checking de l'Epita (travail sur la sémantique de LTL, et écriture d'un model checker jouet en quelques lignes de Python). - la facilité avec laquelle on peut chaîner les différents outils pour construire un pipeline de manipulation d'automates - une technique utilisant un SAT-solver pour synthétiser des automates équivalents mais avec d'autres conditions d'acceptation. 14h45-15h30: Maximilien Colange (ENS de Cachan) Je présenterai TiAMo, un model-checker pour les systèmes temporisés développé au LSV. Les systèmes temporisés présentent une composante en temps continu, qui font de leurs espaces d'états des graphes infinis à branchement infini. Dans le cadre du model-checking, leur analyse repose essentiellement sur des abstractions permettant de se ramener à des graphes discrets. Nous nous concentrons sur les problèmes d'accessibilité dans les automates temporisés, et d'accessibilité optimale dans les automates temporisés à coûts positifs. TiAMo est pensé comme une plateforme permettant la comparaison expérimentale des différents algorithmes et abstractions pour la vérification de systèmes temporisés. Je rappellerai les principaux problèmes algorithmiques qui se posent dans ce cadre, et les différentes solutions qui ont été proposées. Je présenterai également l'outil TiAMo, et les algorithmes d'analyse qu'il implémente. 15h30-16h00: pause café 16h00: vie du groupe ======================================================================== -- Alexandre Duret-Lutz

1 0

New journal publication: TextCatcher: a method to detect curved and challenging text in natural scenes (IJDAR)
by Jonathan Fabrizio 17 Mar '16

17 Mar '16

We are happy to announce that the following paper has been accepted for publication in the International Journal of Document Analysis and Recognition (IJDAR): TextCatcher: a method to detect curved and challenging text in natural scenes Jonathan Fabrizio (1) Myriam Robert-Seidowsky (1) Séverine Dubuisson (2) Stefania Calarasanu (1) Raphaël Boissel (1) (1) EPITA Research and Development Laboratory (LRDE) (2) Sorbonne Universités, UPMC - ISIR In this paper, we propose a text detection algorithm which is hybrid and multi-scale. First, it relies on a connected component-based approach: After the segmentation of the image, a classification step using a new wavelet descriptor spots the letters. A new graph modeling and its traversal procedure allow to form candidate text areas. Second, a texture-based approach discards the false positives. Finally, the detected text areas are precisely cut out and a new binarization step is introduced. The main advantage of our method is that few assumptions are put forward. Thus, “challenging texts” like multi-sized, multi-colored, multi- oriented or curved text can be localized. The efficiency of TextCatcher has been validated on three different datasets: Two come from the ICDAR competition, and the third one contains photographs we have taken with various daily life texts. We present both qualitative and quantitative results.

1 0

[Seminaire-LRDE] Mercredi 23 mars 2016: Joël Falcou, Université Paris Sud, NumScale
by Daniela Becker 15 Mar '16

15 Mar '16

Chers collègues, En mars, nous vous invitons à une deuxième session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) après celle de demain Mercredi 16 mars, où nous recevons Guillaume Torchon, Grenoble-INP & GIPSA-lab, pour parler d’"Analyse hiérarchique d’images multimodales ». Vous pouvez dès à présent noter le 2e rendez-vous du LRDE : Mercredi 23 mars 2016 (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/2016-03-23 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 23 mars 2016 : * 11h: Boost.SIMD - Maximisez votre CPU directement depuis C++ -- Joël Falcou, Université Paris Sud, NumScale https://github.com/NumScale/boost.simd Les extensions multimédia (SSE, AVX, NEON) sont une composante majeure des processeurs d'aujourd'hui qui restent plus que sous-utilisées. Les principales raisons de cette sous-utilisation sont la relative obscurité des jeux d'instructions, leur variété entre et même au sein des différentes familles de puces et surtout, une méconnaissance de la disponibilité des ces unités de calculs. Boost.SIMD est une bibliothèque permettant d'exploiter ces extensions de manière efficace et expressive, facilitant l'utilisation, la diffusion et la portabilité de tels codes, ouvrant la porte à des accélérations de l'ordre de 4 à 10 sur un simple cœur. Cet exposé présentera les fonctionnalités de Boost.SIMD, les challenges posés par son implémentation, comment le C++ moderne répond à plusieurs de ces problèmes et les éléments bloquants qu'il reste à résoudre. -- Joël Falcou est maître de conférences en informatique au LRI, Université Paris Sud. Ses travaux de thèse ont porté sur la programmation parallèle pour la vision artificielle et plus particulièrement sur les applications de la programmation générative pour la création d'outils d'aide à la parallélisation. Il est également conseiller scientifique chez NumScale. 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. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

[Seminaire-LRDE] Mercredi 16 mars 2016: Guillaume Tochon - Grenoble-INP & GIPSA-lab
by Daniela Becker 01 Mar '16

01 Mar '16

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 16 mars 2016 (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/2016-03-16 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 16 mars 2016 : * 11h: Analyse hiérarchique d'images multimodales -- Guillaume Tochon - Grenoble-INP & GIPSA-lab Il y a un intérêt grandissant pour le développement d’outils de traitements adaptés aux images multimodales (plusieurs images de la même scène acquises avec différentes caractéristiques). Permettant une représentation plus complète de la scène en question, ces images multimodales ont de l'intérêt dans plusieurs domaines du traitement d'images. Les exploiter et les manipuler de manière optimale soulève cependant plusieurs questions. Dans cet exposé, nous étendrons les représentations hiérarchiques, outil puissant pour le traitement et l’analyse d’images classiques, aux images multimodales afin de mieux exploiter l’information additionnelle apportée par la multimodalité et améliorer les techniques classiques de traitement d’images. En particulier, nous nous concentrerons principalement sur deux modalités différentes, fréquemment rencontrées dans le domaine de la télédétection: - La modalité spectrale-spatiale, propre aux images hyperspectrales (images à très haute résolution spectrale - plusieurs centaines de canaux). Une intégration adaptée de cette information spectrale-spatiale lors de l'étape de construction de la représentation hiérarchique (en l’occurrence, un arbre de partition binaire) nous permettra par la suite, via un processus de minimisation énergétique, de proposer une carte de segmentation de l'image optimale vis-à-vis de l'opération de démélange spectral. - La modalité sensorielle, c'est-à-dire les images acquises par des capteurs de différentes natures. Ces images "multisources", porteuses d'informations à la fois redondantes et complémentaires, sont particulièrement intéressantes pour des applications de segmentation. Nous proposerons une méthode se basant sur le très récent concept de tresses de partitions (extensions des hiérarchies de partitions classiques) afin de réaliser l'analyse hiérarchique de ces images multisources, et en obtiendrons une segmentation (là encore) via un processus de minimisation énergétique. - Enfin, nous décrirons très brièvement une méthode d'analyse d'images multitemporelles permettant d'effectuer du suivi d'objet, en se basant également sur les représentations hiérarchiques des différentes images de la séquence. -- Guillaume Tochon a obtenu un diplôme d'ingénieur de Grenoble-INP (école ENSE3) en 2012 et un doctorat de l'université de Grenoble Alpes (rattaché au laboratoire GIPSA-lab) en 2015, tous deux en spécialisation ``traitement du signal et des images''. Il est actuellement attaché temporaire d'enseignement et de recherche à Grenoble-INP et conduit ses recherches au sein du département Images et Signaux du GIPSA-lab. Ses activités de recherches se situent à l'intersection entre la morphologie mathématique et la fusion de données, se focalisant notamment sur l'utilisation de représentations hiérarchiques pour l'analyse d'images multimodales, pour diverses applications telles que la segmentation ou le démélange spectral. 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. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0