- Annonce

[Séminaire des étudiants CSI] mercredi 11 juillet 2012 - Amphi 3
by Daniela Becker 03 Jul '12

03 Jul '12

Bonjour, nous avons le plaisir de vous inviter au séminaire des étudiants du LRDE. Il aura lieu le mercredi 11 juillet 2012 à partir de 9h30 en Amphi 3 (KB). ----------------------------------------------------------------------- Au programme : *SPOT, VERIFICATION DU LOCUTEUR, CLIMB, VAUCANSON, OLENA* http://publis.lrde.epita.fr/Seminar-2012-07-11 SPOT * 9h30 : Méthodes de réduction par ordre partiel dans Spot -- Pierre Parutto * 10h00 : Réduction par simulation directe pour les TGBA -- Thomas Badie VERIFICATION DU LOCUTEUR * 10h30 : Séparation de locuteur -- Victor Lenoir 11h - 11h15 : PAUSE * 11h15 : Modèles de mélanges de gaussiennes fondés sur des matrices de covariance pleines -- Benjamin Roux CLIMB * 11h45 : Optimisation en Common Lisp et son application à Climb -- François Ripault * 12h15 : Construction d’une interface pour et avec Climb -- Laurent Senta * 12h45 - 14h00 : PAUSE DEJEUNER VAUCANSON * 14h00 : Vers Vaucanson 2.0 -- David Moreira OLENA * 14h30 : Approche parallèle pour le calcul de l'arbre des formes en n-dimensions -- Sébastien Crozet * 15h00 : Extraction de texte avec des ondelettes -- Raphael Boissel * 15h30 - 15h45 : PAUSE * 15h45 : Améliorer Horn-Schunck -- Sylvain Lobry * 16h15 : Inpainting rapide préservant la structure -- Coddy Levi Les Résumés des exposés : ************************** SPOT * 9h30 : Méthodes de réduction par ordre partiel dans Spot -- Pierre Parutto Spot est une bibliothèque de model checking implémentant une approche par automates. Pour le moment les algorithmes de vérification de propriétés dans Spot utilisent l’espace d’états sans réduction du système. Ils souffrent donc de l’explosion combinatoire de la taille de ce dernier. Une manière de résoudre ce problème est d’utiliser des méthodes de réduction par ordre partiel. Ces méthodes permettent d’ignorer certains comportements équivalents du système pour une certaine propriété. Ainsi il est possible de réduire la taille de l’espace d’états généré tout en conservant le même comportement général. Le but de ce travail est d’évaluer comment ces méthodes d’ordre partiel peuvent être intégrées dans Spot. * 10h00 : Réduction par simulation directe pour les TGBA -- Thomas Badie L’approche par automates du model checking s’appuie traditionnellement sur des Automates de Büchi (BA) qu’on souhaite les plus petits possible. Etessami et al. ont présenté une méthode de réduction d’un BA basée sur une relation de simulation (dite directe) entre ses états. Spot, bibliothèque de model checking, utilise principalement des TGBA qui généralisent les BA. Nous montrons qu’en adaptant cette simulation aux TGBA on obtient des automates plus concis que les BA équivalents. Cette nouvelle technique est incluse dans Spot 0.9 et a permis de produire des automates plus petits que dans les précédentes versions. VERIFICATION DU LOCUTEUR * 10h30 : Séparation de locuteur -- Victor Lenoir La séparation de locuteur et la détection de voix jouent un important rôle dans les systèmes de reconnaissance du locuteur, principalement dans le cas d’un signal à plusieurs locuteurs. Nous allons présenter une méthode de séparation de locuteur basée sur des méthodes variationnelles et sur les speaker factors tel que décrite dans l’état de l’art de systèmes de reconnaissance du locuteur. Afin de tester les performances de cette méthode un ensemble de tests sera effectué sur les données interview de NIST-SRE 2010. 11h - 11h15 : PAUSE * 11h15 : Modèles de mélanges de gaussiennes fondés sur des matrices de covariance pleines -- Benjamin Roux Le modèle du monde représenté par les mélanges de gaussiennes (UBM - GMM) est l’approche état de l’art pour les systèmes de vérification du locuteur. On utilise généralement des matrices de covariance diagonale. Cette simplification permet d’avoir un apprentissage rapide des différents modèles. Nous allons explorer le cas des matrices de covariance pleines. On va présenter la complexité additionelle et les gains en termes de performances. Toutes les expériences seront menées sur des données issues de NIST-SRE 2010. CLIMB * 11h45 : Optimisation en Common Lisp et son application à Climb -- François Ripault Common Lisp est un langage de programmation dynamique. Bien qu’il ne soit pas a priori axé sur la performance, il s’avère que le langage offre certaines fonctionnalités liées à l’optimisation. Cependant, le gain en performance a un impact sur la généricité du code, l’optimisation limitant celle-ci. Climb est une bibliothèque de traitement d’image écrite dans ce langage, ayant pour objectif de se comparer à des équivalents écrits dans des langages statiques tels que C++. L’objectif est de profiter de la généricité qu’offre Common Lisp pour l’écriture d’une bibliothèque de traitement d’image. Mais une telle bibliothèque a également des contraintes de performance, il s’agit donc de trouver un terrain d’entente entre ces deux aspects. Nous présenterons les différentes fonctionnalités qu’offre Common Lisp pour optimiser un programme, et leur utilisation dans Climb pour rendre la bibliothèque plus rapide, sans pour autant diminuer sa généricité. Nous présenterons également les premiers résultats du travail d’optimisation dans Climb, le travail restant et les apports de l’utilisation de Common Lisp pour une telle tâche. * 12h15 : Construction d’une interface pour et avec Climb -- Laurent Senta Climb est une bibliothèque de traitement d’image générique. Encore à l’état de prototype, Climb fournit déjà un certain nombre d’outils comme les morphers et l’opérateur $ qui permettent de simplifier la définition de chaînes d’algorithmes. Afin de prolonger cet aspect, une interface graphique a été développée. Celle-ci permet de construire des chaînes de traitement d’image sans connaissance en programmation, tout en offrant un retour à la fois visuel et interactif. Notre approche utilise les algorithmes et outils définis dans la bibliothèque pour construire la logique interne de l’application ainsi que ses différents aspects interactifs. La généricité étant l’une des caractéristiques principales de Climb, nous avons été capables d’étendre son champ d’application au-delà du traitement d’image et ainsi montrer qu’elle peut être utilisée dans des situations différentes telles que la construction d’une interface graphique. * 12h45 - 14h00 : PAUSE DEJEUNER VAUCANSON * 14h00 : Vers Vaucanson 2.0 -- David Moreira Vaucanson est une plate-forme de manipulation d’automates et de transducteurs dont l’interface et le développement se sont montrés complexes et inefficaces. Des travaux de spécifications et de design ont été effectués afin d’avoir un coeur efficace en terme de développement et de vitesse. Cette version 2.0 de Vaucanson est actuellement en développement. Ce rapport présente la version 2.0 de Vaucanson et son utilisation par le portage de deux algorithmes : l’évaluation d’un mot par un automate et la déterminisation d’automates. Dans une seconde partie, nous montrerons si Vaucanson 2.0 tient ses promesses en termes de vitesse d’exécution. OLENA * 14h30 : Approche parallèle pour le calcul de l'arbre des formes en n-dimensions -- Sébastien Crozet L’arbre des formes est une transformée d’image utile pour effectuer des traitements sur des images discrètes de façon auto-duale. Un algorithme (non publié), travaillant sur des images n-dimensionnelles dans l’espace des complexes cellulaires, nous permet déjà de construire un arbre des formes en temps quasi-linéaire. Cependant, cet algorithme reste souvent largement plus lent que d’autres approches en temps (n log(n)) sur des images naturelles en 2D ou 3D, le nombre de cellules à traiter dans l’espace des complexes étant très élevé. En vue d’améliorer ces temps de calculs, nous présentons une approche pour paralléliser l’algorithme de calcul d’arbre quasi-linéaire en exhibant des propriétés topologiques et algorithmiques qui ne peuvent être facilement obtenues par les autres approches existantes. * 15h00 : Extraction de texte avec des ondelettes -- Raphael Boissel Nous allons présenter une méthode permettant de différencier le texte du non-texte dans une image en utilisant des descripteurs inspirés des algorithmes de compression de données. L’objectif principal de cette approche est de calculer un signal qui va permettre à des systèmes d’apprentissage supervisés (comme des kppv ou des machines à vecteurs de support) de classifier le texte et le fond d’une image. Afin de calculer ce signal, nous utiliserons des méthodes à base d’ondelettes similaires à celles utilisées dans les formats de compression jpeg ou png. Nous allons également étudier quelles ondelettes produisent les meilleurs résultats, avec quel système d’apprentissage et comparer cela avec d’autres descripteurs, qui ne sont pas à base d’ondelettes. Enfin, nous verrons comment il est possible de diminuer le temps de calcul nécessaire pour ces descripteurs en utilisant l’élévation en ondelette et des méthodes optimisées pour calculer l’image polaire. * 15h30 - 15h45 : PAUSE * 15h45 : Améliorer Horn-Schunck -- Sylvain Lobry Calculer le flux optique a de nombreuses applications telles que l’estimation de mouvement ou un premier pas vers l’inpainting vidéo. L’équation du flux optique ne peut pas être résolue telle quelle à cause du problème de fenêtrage (deux inconnues pour une seule équation). Un ensemble d’algorithme essaie de résoudre cette équation en se basant sur une stratégie globale, c’est-à-dire en essayant d’avoir des petites variations dans le flux. Le premier d’entre eux est l’algorithme d’Horn- Schunck. Celui-ci, même s’il marche dans de nombreux cas, a plusieurs inconvénients, y compris celui d’être lent et de ne pas pouvoir trouver les grands déplacements. Dans le but de résoudre ces problèmes, plusieurs stratégies ont été développées. Nous présenterons la méthode et analyserons les bénéfices apportés en appliquant une stratégie multi-échelle à l’algorithme d’Horn-Schunck. * 16h15 : Inpainting rapide préservant la structure -- Coddy Levi L’inpainting consiste à réparer des parties d’une image de façon visuellement plausible. Son but peut être de réparer des régions endommagées, ou de supprimer des objets tels que du texte superposé à une vidéo. De nombreuses approches ont été proposées pour répondre au problème dans le cas de petites ou de larges régions. Cependant la plupart d’entre elles ne sont pas adaptées à des applications en temps réel. Nous proposons une méthode plus simple basée sur la reconstruction de structure et la diffusion des couleurs afin de répondre au problème dans une optique de temps réel. -- Daniela Becker Responsable administrative du LRDE

1 0

Séminaire Performance et Généricité du LRDE le mercredi 4 juillet 2012
by Daniela Becker 28 Jun '12

28 Jun '12

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 4 juillet 2012 (14h00-17h00). Au programme: * 14h: Vérification efficace de propriétés insensibles au bégaiement. -- Ala Eddine Ben Salem (doctorant) Le model checking est une technique de vérification formelle automatique. Prenant en entrée un modèle décrivant toutes les exécutions possibles du système et une propriété exprimée sous la forme d'une formule de logique temporelle, un algorithme de model checking répond si le modèle satisfait ou non la formule. Le problème principal du model-checking est l'explosion combinatoire de l'espace d'états décrivant le système. Afin d'améliorer les performances, on a apporté les contributions suivantes à l'approche automate du model checking. D'abord l'amélioration de l'algorithme de vérification en deux passes de l'approche basée sur les automates Testeur TA (Testing Automaton). Ensuite la proposition d'une méthode permettant de transformer un automate TA en un automate vérifiable en une seule passe, qu'on a appelé STA (Single-pass Testing Automaton). Enfin, la contribution la plus significative est un nouveau type d'automate baptisé TGTA (Transition-based Generalized Testing Automaton). L'apport principal de cette nouvelle approche consiste à proposer une méthode permettant de supprimer les transitions bégayantes dans un TGTA sans avoir besoin, ni d'ajouter une seconde passe comme dans l'approche TA, ni d'ajouter un état artificiel comme dans l'approche STA. -- A.E. Ben Salem est ingénieur ENSEEIHT-2005 en Informatique et Mathématiques Appliquées, il a obtenu en parallèle un Master Recherche Sûreté du Logiciel et Calcul à haute Performance à l’INP Toulouse. Depuis 2011, il est doctorant au LRDE et au LIP6 sur la vérification formelle de propriétés sur des systèmes logiciels, en lien avec le projet Spot. * 14h30: Composition dynamique de techniques pour le model checking efficace -- Étienne Renault (doctorant) Le model checking est une technique qui permet de s'assurer qu'un système vérifie un ensemble de caratéristiques appelées propriétés. Le système et la négation de la formule sont ensuite représentés de manière abstraite (ici un automate) pour pouvoir détecter des comportements incohérents. Ces propriétés ont été classifiées et possèdent des particularités qui peuvent être exploitées afin de réduire la complexité du processus de vérification. Nous montrerons ici comment tirer parti dynamiquement des différentes classes de formules. -- E. Renault est diplômé de Paris VI en système et applications réparties, il s'intéresse à la vérification formelle des systèmes concurents. Il a intégré cette année le LRDE dans le cadre de sa thèse portant sur la composition dynamique de techniques pour le model checking efficace. Ce travail, en collaboration avec l'équipe MoVe du Lip6, s'intègre au projet Spot. * 15h30: Filtrage morphologique dans les espaces de formes : Applications avec la représentation d'image par arbres -- Yongchao Xu (doctorant) (Morphological Filtering in Shape Spaces: Applications using Tree-Based Image Representations) Connected operators are filtering tools that act by merging elementary regions of an image. A popular strategy is based on tree-based image representations: for example, one can compute a shape-based attribute on each node of the tree and keep only the nodes for which the attribute is sufficiently strong. This operation can be seen as a thresholding of the tree, seen as a graph whose nodes are weighted by the attribute. Rather than being satisfied with a mere thresholding, we propose to expand on this idea, and to apply connected filters on this latest graph. Consequently, the filtering is done not in the image space, but in the space of shapes built from the image. Such a processing is a generalization of the existing tree-based connected operators. Indeed, the framework includes classical existing connected operators by attributes. It also allows us to propose a class of novel connected operators from the leveling family, based on shape attributes. Finally, we also propose a novel class of self-dual connected operators that we call morphological shapings. -- Yongchao Xu received the B.S. degree in optoelectronic engineering from Huazhong University of Science and Technology, China, in 2008, the "diplôme d'ingénieur" in electronic & embedded system at Polytech' Paris-Sud and the M.S. degree in signal & image processing from Université Paris Sud, in 2010. He is currently a PhD student at Université Paris Est working on image segmentation, morphological image analysis and, especially shape-based connected morphology. 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

1 0

Tutorial at ILC 2012
by Didier Verna 25 Jun '12

25 Jun '12

Hello, it is my pleasure to announce that I will hold a 2 hours tutorial on Lisp extensibility and its impact on DSL implementation at the next International Lisp Conference, Kyoto, Japan, October 2012. For more information, please consult: http://international-lisp-conference.org/2012/tutorials.html -- 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

1 0

L'air de rien 25.0
by Daniela Becker 23 May '12

23 May '12

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°25 du bulletin du LRDE. C'est un numéro spécial dédié aux parcours professionnels d'anciens élèves du LRDE depuis la promo 2000 jusqu'à celle de 2011. Vous y trouverez également les dernières publications et nouvelles du LRDE. Vous pouvez télécharger le bulletin en couleur à la page suivante : http://publis.lrde.epita.fr/201205-l-air-de-rien-25 -- Daniela Becker Responsable administrative du LRDE

1 0

[Seminaire-LRDE] Séminaire Performance et Généricité du LRDE le mercredi 20 juin 2012
by Daniela Becker 23 May '12

23 May '12

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 20 juin 2012 (14h00-16h00). Au programme: * 14h00: GPU Computing : début d'une ère ou fin d'une époque ? -- Eric Mahé, responsable du projet OpenGPU L'arrivée des GPU (Graphics Processing Unit) a profondément changé la manière de concevoir la notion de coprocesseur. A moins de 500€, il est désormais possible d'avoir à sa disposition une puissance de calcul qui n'était réservée jusqu'à un passé récent qu'aux grands centres de calcul. La société Nvidia, en mettant au point l'environnement CUDA, a fourni à la communauté des développeurs des moyens simples et efficaces pour rendre cette puissance de calcul accessible au plus grand nombre. Depuis, sous l'impulsion de la société Apple, le standard OpenCL est venu ouvrir la voie d'une véritable parallélisation des applications sur l'ensemble des ressources processeur offertes aux développeurs. Cet exposé décrira les différentes technologies permettant la programmation parallèle des GPU en mettant l'accent sur les contraintes actuelles et les progrès à venir des futures architectures comme le processeur Kepler. Des démonstrations ainsi que des exemples de code viendront compléter cet exposé. -- Eric Mahé a été responsable des nouvelles technologies au sein de l'équipe marketing de Sun France pendant 20 ans après avoir occupé différents postes de chef de projet dans le domaine du nucléaire et de la défense. Son rôle fut d'évangéliser les choix technologiques et stratégiques de Sun auprès des communautés concernées par le langage Java, les développements du Logiciel Libre et les applications citoyennes de la fédération d'identité basées sur le projet Liberty Alliance. Diplômé de plusieurs troisièmes cycles en marketing, biologie et informatique, Eric Mahé est administrateur de l'association Silicon Sentier, expert auprès du pôle de compétitivité CAP Digital et professeur de communication à l'université René Descartes – Paris V. -- Eric Mahé assure depuis 2009 la direction du projet OpenGPU dont l'objectif est la mise au point de nouvelles chaînes de compilation à destination des architectures hybrides GPU/CPU et a fondé la société MassiveRand spécialisée dans les nombres aléatoires dans le domaine de la sécurité. 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

1 0

[CfP] ACM SAC'13 PL
by Didier Verna 22 May '12

22 May '12

CALL FOR PAPERS SAC'13 - ACM 2013 SYMPOSIUM ON APPLIED COMPUTING Technical Track on "Programming Languages" March 18-22, 2013 Coimbra, Portugal SAC '13 Over the past 27 years, the ACM Symposium on Applied Computing has become a primary forum for applied computer scientists, computer engineers, software engineers, and application developers from around the world to interact and present their work. SAC 2013 is sponsored by the ACM Special Interest Group on Applied Computing (SIGAPP). For additional information, please check the SAC web page: http://www.acm.org/conferences/sac/sac2013/. This document is also available at: http://www.cse.unt.edu/~bryant/sac2013/PL-SAC13-CFP.pdf PROGRAMMING LANGUAGES (PL) TRACK A technical track on Programming Languages will be held at SAC'13. It will be a forum for engineers, researchers and practitioners throughout the world to share technical ideas and experiences relating to implementation and application of programming languages. Original papers and experience reports are invited in all areas of programming languages. Major topics of interest include but are not limited to the following: − Compiling Techniques, − Domain-Specific Languages, − Formal Semantics and Syntax, − Garbage Collection, − Language Design and Implementation, − Languages for Modeling, − Model-Driven Development and Model Transformation, − New Programming Language Ideas and Concepts, − New Programming Paradigms, − Practical Experiences with Programming Languages, − Program Analysis and Verification, − Program Generation and Transformation, − Programming Languages from All Paradigms (Agent-Oriented, Aspect-Oriented, Functional, Logic, Object-Oriented, etc.), − Visual Programming Languages. GUIDELINES FOR SUBMISSION Paper submissions must be original, unpublished work. Submissions should be in electronic format, via the START site: https://www.softconf.com/c/sac2013/. Author(s) name(s) and address(es) must not appear in the body of the paper, and self-reference should be avoided and made in the third person. Submitted papers will undergo a blind review process. Authors of accepted papers should submit an editorial revision of their papers that fits within six two-column pages (an extra two pages, to a total of eight pages, may be available at a charge). Please comply with this page limitation already at submission time. For accepted papers, registration for the conference is required and allows accepted papers to be printed in the conference proceedings. For each accepted paper, an author or a proxy attending SAC MUST present the paper. This is a requirement for the paper to be included in the ACM/IEEE digital library. A set of selected papers, which did not get accepted as full papers, will be accepted as poster papers and will be published as extended 2-page abstracts in the symposium proceedings. After the conference, selected accepted papers will be invited to a special issue of the Computer Languages, Systems and Structures journal (http://www.journals.elsevier.com/computer-languages-systems-and-structures/) IMPORTANT DATES September 21, 2012: Full Paper Submissions November 10, 2012: Author Notification November 30, 2012: Camera-Ready Copy The SAC 2013 Programming Language Track Program Committee Members Vasco Amaral, Universidade Nova de Lisboa, Portugal Roberto da Silva Bigonha, Universidade Federal de Minas Gerais, Brasil Haiming Chen, Chinese Academy of Sciences, China Johan Fabry, University of Chile, Chile Sebastian Guenter, Vrije Universiteit Brussel, Belgium Gopal Gupta, University of Texas at Dallas, USA Christian Haack, University of Nijmegen, The Netherlands Christian Hammer, Saarland University, Germany Matthias Hauswirth, University of Lugano, Switzerland Pedro Henriques, University of Minho, Portugal Michael Hind, IBM, USA Nigel Horspool, University of Victoria, Canada Zoltan Horvath, Eotvos Lorand University, Hungary Bo Huang, Intel, China Geylani Kardas, Ege University, Turkey Shih Hsi "Alex" Liu, California State University, Fresno, USA Hanspeter Moessenboeck, Johannes Kepler Universitat Linz, Austria Jesús García Molina, University of Murcia, Spain Nikolaos Papaspyrou, National Technical University of Athens, Greece Corneliu Popeea, Technical University of Munich, Germany Andre Santos, Universidade Federal de Pernambuco, Brazil Bostjan Slivnik, University of Ljubljana, Slovenia Didier Verna, EPITA, France Wuu Yang, National Chiao-Tung University, Taiwan Youtao Zhang, University of Pittsburgh, USA Track Chairs Marjan Mernik, University of Maribor, Slovenia, marjan.mernik(a)uni-mb.si Barrett Bryant, University of North Texas, USA, Barrett.Bryant(a)unt.edu -- 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

1 0

Spot 0.9 is released
by Alexandre Duret-Lutz 09 May '12

09 May '12

We are pleased to announce the release of Spot 0.9. 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. You can find the new release here: http://spot.lip6.fr/dl/spot-0.9.tar.gz (11MB) The major news in this release are all related to the logic-to-Büchi-automaton translation engine: 1. The linear-time fragment of PSL is supported. This first implementation, enough to experiment with the logic, shall be improved in future versions. (Feedback most welcome.) 2. The LTL simplification code has been overhauled and augmented with new rules. 3. A new simulation-based post-processing can be used to simplify the TGBA constructed. For more details about the first two points (supported operators, and rewritings performed), please read the file doc/tl/tl.pdf included in spot-0.9.tar.gz. A consequence of the last two points is that Spot 0.9 is faster than Spot 0.8.3 and can produce even smaller automata. For some comparative benchmarks, please download http://spot.lip6.fr/dl/bench-0.9.pdf Please direct any feedback and questions to <spot(a)lrde.epita.fr>. (Subscribe at https://www.lrde.epita.fr/mailman/listinfo/spot if you wish.) A more detailed list of new features follows. New in spot 0.9 (2012-05-09): * New features: - Operators from the linear fragment of PSL are supported. This basically extends LTL with Sequential Extended Regulat Expressions (SERE), and a couple of operators to bridge SERE and LTL. See doc/tl/tl.pdf for the list of operators and their semantics. - Formula rewritings have been completely revamped, and augmented with rules for PSL operators (and some new LTL rules as well). See doc/tl/tl.pdf for the list of the rewritings implemented. - Some of these rewritings that may produce larger formulas (for instance to rewrite "{a;b;c}" into "a & X(b & Xc)") may be explicitely disabled with a new option. - The src/ltltest/randltl tool can now generate random SEREs and random PSL formulae. - Only one translator (ltl2tgba_fm) has been augmented to translate the new SERE and PSL operators. The internal translation from SERE to DFA is likely to be rewriten in a future version. - A new function, length_boolone(), computes the size of an LTL/PSL formula while considering that any Boolean term has length 1. - The LTL/PSL parser recognizes some UTF-8 characters (like ◇ or ∧) as operators, and some output routines now have an UTF-8 output mode. Tools like randltl and ltl2tgba have gained an -8 option to enable such output. See doc/tl/tl.pdf for the list of recognized codepoints. - A new direct simulation reduction has been implemented. It works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, and it can be tested via ltl2tgba's -RDS option. - unabbreviate_wm() is a function that rewrites the W and M operators of LTL formulae using R and U. This is called whenever we output a formula in Spin syntax. By combining this with the aforementioned PSL rewriting rules, many PSL formulae that use simple SERE can be converted into LTL formulae that can be feed to tools that only understand U and R. The web interface will let you do this. - changes to the on-line translator: + SVG output is available + can display some properties of a formula + new options for direct simulation, larger rewritings, and utf-8 output - configure --without-included-lbtt will prevent LBTT from being configured and built. This helps on systems (such as MinGW) where LBTT cannot be built. The test-suite will skip any LBTT-based test if LBTT is missing. * Interface changes: - Operators ->, <->, U, W, R, and M are now parsed as right-associative to better match the PSL standard. - The constructors for temporal formulae will perform some trivial simplifications based on associativity, commutativity, idempotence, and neutral elements. See doc/tl/tl.pdf for the list of such simplifications. - Formula instances now have many methods to inspect their properties (membership to syntactic classes, absence of X operator, etc...) in constant time. - LTL/PSL formulae are now handled everywhere as 'const formula*' and not just 'formula*'. This reflects the true nature of these (immutable) formula objects, and cleanups a lot of code. Unfortunately, it is a backward incompatible change: you may have to add 'const' to a couple of lines in your code, and change 'ltl::const_vistitor' into 'ltl::visitor' if you have written a custom visitor. - The new entry point for LTL/PSL simplifications is the function ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. The ltl_simplifier class implements a cache. Functions such as reduce() or reduce_tau03() are deprecated. - The old game-theory-based implementations for direct and delayed simulation reductions have been removed. The old direct simulation would only work on degeneralized automata, and yet produce results inferior to the new direct simulation introduced in this release. The implementation of delayed simulation was unreliable. The function reduc_tgba_sim() has been kept for compatibility (it calls the new direct simulation whatever the type of simulation requested) and marked as deprecated. ltl2tgba's options -Rd, -RD are gone. Options -R1t, -R1s, -R2s, and -R2t are deprecated and all made equivalent to -RDS. - The tgba_explicit hierarchy has been reorganized in order to make room for sba_explicit classes that share most of the code. The main consequence is that the tgba_explicit type no longuer exists. However the tgba_explicit_number, tgba_explicit_formula, and tgba_explicit_string still do.

1 0

Séminaire MeFoSyLoMa du 2012-05-04 à l'Epita
by Alexandre Duret-Lutz 30 Apr '12

30 Apr '12

======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/j2012-05-04.html Méthodes Formelles pour Les Systèmes Logiciels et Matériels Vendredi 4 mai 2012, 14h-17h Adresse : Epita, Amphi 4 (derrière la verrière à gauche dans la cour) 24 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : http://maps.google.fr/maps?q=48.815379,2.363139 http://www.lrde.epita.fr/~adl/dl/lrde-amphi4.pdf ======================================================================== 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-15h00 (Amphi 4) : Serge Haddad (LSV) Synthesis and Analysis of Product-form Petri Nets For a large Markovian model, a “product form” is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1) we provide a sound and complete set of rules for the synthesis; (2) we characterise the exact complexity of classical problems like reachability; (3) we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed. 15h00-15h30 (Amphi 4) : Samira Chaou (LACL) Modélisation et analyse d'un système de notation dans un système de stockage pair-à-pair. Dans un système de stockage de données distribué, la disponibilité des données est une propriété critique à assurer. Pour analyser la robustesse du système de stockage UbiStorage on a procédé à l'évaluation de ce dernier en présence d'attaquants internes en utilisant la simulation. Pour résoudre le problème de perte de données ainsi détecté, un système de réputation est mis en place. Dans cet exposé, nous allons voir l'utilisation du formalisme ABCD pour la modélisation du système de stockage pair-à-pair d'UbiStorage et la modélisation des différentes attaques ainsi que du système de notation. Nous allons aussi voir les résultats d'analyse par model-checking du système de notation. 15h30-16h00 (LRDE) : pause café Elle aura lieu dans la bibliothèque du LRDE, au 18 rue Pasteur (2e étage). 16h00: vie du groupe (dans une salle voisine). ======================================================================== -- Alexandre Duret-Lutz

1 0

[Seminaire-LRDE] Séminaire Performance et Généricité du LRDE le mercredi 9 mai 2012
by Daniela Becker 25 Apr '12

25 Apr '12

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 9 mai 2012 (14h00-17h30). Au programme: * 14h00: Un modèle générique de traitement et de représentation des images -- Antoine Manzanera http://www.ensta-paristech.fr/~manzaner Concilier généricité et performance des systèmes de vision a toujours été au cœur des préoccupations scientifiques du laboratoire d'Électronique et Informatique d'ENSTA-ParisTech. Nous y avons abordé ce problème sous différents points de vue: électronique, algorithmique, et logiciel. Depuis nos travaux sur les rétines programmables et leur algorithmique exotique, nous avons progressivement intégré la multiplicité des modèles et structures de données, ainsi que l'emprise des architectures sur étagères, pour appréhender l'hétérogénéité des systèmes multi-plateformes. Dans cette présentation à deux voix, on abordera le problème sous deux angles complémentaires, l'un touchant au modèle et aux algorithmes, l'autre au logiciel et aux plateformes de calcul. Ce premier exposé présente un modèle générique de traitement et de représentation des images fondé sur les espaces de caractéristiques "local jets" (LJ, ou dérivées partielles multi-échelles), comme exemple de cadre algorithmique unifié. Grâce à un espace où la métrique naturelle est directement liée à la similarité visuelle, ce cadre permet d'aborder un grand nombre d'opérateurs de traitement d'images de bas niveau, qui correspondent généralement à la rétro-projection dans l'espace image de points de l'espace des caractéristiques transformé. Il permet aussi d'aborder des représentations visuelles de plus haut niveau (modèles d'objet par exemple) à partir de statistiques globales extraites de l'espace des caractéristiques. On justifiera cette représentation et on l'illustrera par diverses applications : Moyennes non locales (NL-Means) par Convolution dans l'espace LJ pour le débruitage de vidéos, Calcul du flux optique par recherche du plus proche voisin dans l'espace LJ, Modélisation de fond statique par échantillonnage de l'espace LJ, Détection d'objets par transformée de Hough dense... -- Antoine Manzanera est diplômé de l'Université Claude Bernard à Lyon (Licence de Maths 1991 et Master d'Informatique Fondamentale 1993), et Docteur de Télécom-ParisTech en Signal et Images ("Vision artificielle rétinienne", 2000). Depuis 2001 il est Enseignant-Chercheur à l'ENSTA-ParisTech. Dans ses recherches, il s'intéresse au Traitement d'Images et à la Vision de bas niveau, du modèle mathématique à l'implantation parallèle sur un système embarqué. Il enseigne principalement en 2ème et 3ème année du cycle Ingénieur ENSTA, et dans le Master d'Informatique de l'UMPC (Paris 6), dans les spécialités Imagerie et IAD. * 15h30: Analyse des mouvements apparents dans un flux vidéo -- Matthieu Garrigues http://www.ensta-paristech.fr/~garrigues Dans ce second exposé, Matthieu Garrigues parlera de ses travaux sur l'analyse des mouvements apparents dans un flux vidéo. La primitive de base, présentée dans un séminaire précédent, permet le suivi temps réel (supérieur à 30 images par seconde) de plusieurs milliers de particules. Ces travaux nous ont permis de développer un cadre générique facilitant l'analyse de scènes dynamiques prises de caméras fixes ou mobiles. Nous montrerons comment cette brique logicielle a été utilisée dans deux exemples d'applications : L'extraction des plans principaux et l'estimation de la profondeur dans un système mono-caméra. Le suivi de particules a été implémenté sur processeurs graphiques avec le framework CUDA, et sur CPU-multicœurs avec OpenMP. Nous expliquerons comment C++ a été utilisé pour factoriser un maximum de code entre ces deux implémentations. -- 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 sur des architectures parallèles. Il est actuellement ingénieur de recherche à l'unité d'électronique et d'informatique de l'ENSTA, où il travaille sur l'analyse temps réel de scènes acquises par des systèmes mobiles mono-caméra. 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

1 0

TUG 2012 paper
by Didier Verna 21 Mar '12

21 Mar '12

Dear all, I'm happy to inform you that my contribution to the next TeX Users Group international conference, TUG 2012, has been accepted. Please find the title and abstract below. Star TeX, the Next Generation In 2010, I asked Donald Knuth why he chose to design and implement TeX as a macro-expansion system (as opposed to more traditional procedure calls). His answer was that: 1/ he wanted something relatively simple for his secretary who was not a computer scientist, 2/ the very limited computing resources at that time practically mandated the use of something much lighter than a true programming language. The first part of the answer left me with a slight feeling of skepticism. It remains to be seen that TeX is simple to use, and when or where it is, its underlying implementation has hardly anything to do with it. The second part of the answer, on the other hand, was both very convincing and arguably now obsolete as well. Time has passed and the situation today is very different from what it was 50 years ago. The available computing power has grown exponentially, and so has our overall skills in language design and implementation. Several ideas on how to modernize TeX already exist. Some have been actually implemented. In this talk, I will present mine. Interestingly enough, it seems to me that modernizing TeX can start with grounding it in an old yet very modern programming language: Common Lisp. I will present the key features that make this language particularly well suited to the task, emphasizing on points such as extensibility, scriptability and multi-paradigm programming. The presentation will include reflections about the software engineering aspects (internals), as well as about the surface layer of TeX itself. Most notably, I will explore the possibilities of providing a more consistent syntax to the TeX API, while maintaining backward compatibility with the existing code base. -- 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

1 0