Annonce January 2016

annonce@lrde.epita.fr

2 participants
4 discussions

publications: two papers accepted at Spin'15

by Alexandre Duret-Lutz

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

8 years, 6 months

[CfP] 9th European Lisp Symposium, May 9-10, Krakow, Poland

by Didier Verna

ELS'16 - 9th European Lisp Symposium Department of Computer Science AGH University of Science and Technology Kraków, Poland May 9-10, 2016 In cooperation with: ACM SIGPLAN Sponsored by EPITA, Franz Inc., LispWorks Ltd. and Dept. of Computer Science AGH UST http://www.european-lisp-symposium.org/ Recent news: - Submission deadline in less than a month! - 3nd invited speaker announced: Stephan Karpinski on Julia: to Lisp or Not to Lisp? 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 9th 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 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. The conference proceedings will be published in the ACM Digital Library. Important dates: - 19 Feb 2016 Submission deadline - 25 Mar 2016 Notification of acceptance - 15 Apr 2016 Early registration deadline - 22 Apr 2016 Final papers due - 9-10 May 2016 Symposium Programme chair: Irène Durand, LaBRI, University of Bordeaux, France Local chair: Michał Psota, Emergent Network Defense, Kraków, Poland Programme committee: Antonio Leitao — INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Portugal Charlotte Heerzel — IMEC, Leuven, Belgium Christian Queinnec — University Pierre et Marie Curie, Paris 6, France Christophe Rhodes — Goldsmiths, University of London, United Kingdom Didier Verna — EPITA Research and Development Laboratory, France Erick Gallesio — University of Nice-Sophia Antipolis, France François-René Rideau, Google, USA Giuseppe Attardi — University of Pisa, Italy Henry Lieberman — MIT, USA Kent Pitman, HyperMeta Inc., USA Leonie Dreschler-Fischer — University of Hamburg, Germany Pascal Costanza — Intel Corporation, Belgium Robert Strandh — University of Bordeaux, France Search Keywords: #els2016, ELS 2016, ELS '16, European Lisp Symposium 2016, European Lisp Symposium '16, 9th ELS, 9th European Lisp Symposium, European Lisp Conference 2016, European Lisp Conference '16 -- @-quartet live: Sunset/Sunside, Paris, Jan 26 2016 ! Book now: http://www.sunset-sunside.com/2016/1/artiste/2101/3453/ Lisp, Jazz, Aïkido: http://www.didierverna.info

8 years, 11 months

[Seminaire-LRDE] Subject: Mercredi 27 janvier 2016: Pierre-Yves Strub -- IMDEA Software Institute - Espagne

by Daniela Becker

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 27 janvier 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-01-27 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 27 janvier 2016 : * 11h: Une introduction à la preuve formelle de sécurité -- Pierre-Yves Strub -- IMDEA Software Institute - Espagne http://www.strub.nu La cryptographie joue un rôle clé dans la sécurité des infrastructures de communication. Il est donc d'une importance capitale de construire des systèmes cryptographiques apportant de fortes garanties de sécurité. C'est dans ce but que les constructions cryptographiques sont étudiées scrupuleusement et viennent avec une preuve de sécurité bornant la probabilité qu'un adversaire casse le crypto-système. La majorité des preuves de sécurité sont réductionnistes: elles construisent, à partir d'un adversaire PPT (Probabilistic Polynomial-Time) violant avec une probabilité écrasante la sécurité de la construction cryptographique, un second adversaire PPT cassant une hypothèse de sécurité. Cette approche, connue sous le nom de "sécurité formelle", permet sur le principe de fournir des preuves mathématiques rigoureuses et détaillées de sécurité. Les récentes constructions cryptographiques (et donc leur analyse de sécurité) sont de plus en plus complexes, et il n'est pas rare qu'elles incluent maintenant la preuve sécurité de l'implémentation du crypto-système, ou de sa résistance aux canaux cachés. En conséquence, les preuves de sécurité de ces algorithmes présentent un niveau de complexité tel qu'un grand nombre d'entre elles sont fausses --- prouvant la sécurité d'une construction qui ne l'est pas. Une solution prometteuse pour pallier ce problème est de développer des outils formels d'aide à la construction et vérification de crypto-systèmes. Bien que de nombreux outils existent pour la cryptographie symbolique, peu d'effort a été fait pour la cryptographie calculatoire --- pourtant utilisée largement parmi les cryptographes. Après avoir introduit le domaine de la preuve formelle et de la sécurité formelle, je présenterai EasyCrypt, un outil d'aide à la preuve des constructions cryptographiques dans le modèle calculatoire. EasyCrypt adopte une approche reposant sur la formalisation de constructions cryptographiques à partir de code concret, dans laquelle la sécurité et les hypothèses de sécurité sont modélisées à partir de programmes probabilistes et où les adversaires sont représentés par du code non spécifié. Une telle approche permet l'utilisation d'outils existants pour la vérification de programmes. EasyCrypt est développé conjointement entre l'IMDEA Software Institute et Inria. -- Pierre-Yves Strub est chercheur au "IMDEA Software Institute", institut madrilène de recherche en informatique. En 2008, il obtient une thèse en informatique de l'École Polytechnique, puis rejoint l'équipe FORMES du laboratoire commun INRIA-Tsinghua University (Pékin, Chine). Avant d'intégrer IMDEA en 2012, il passe deux ans au laboratoire commun MSR-INRIA (Paris, France). Ses recherches portent sur les méthodes formelles, la logique en informatique, la vérification de programmes, la sécurité formelle et la formalisation des mathématiques. -- Depuis qu'il a rejoint IMDEA, ses recherches portent principalement sur la preuve formelle assistée par ordinateur en sécurité/cryptographie. Il est l'un des principaux concepteur et développeur d'EasyCrypt, un outil dédié à la preuve de sécurité de constructions cryptographiques. 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

8 years, 11 months

[Séminaire des étudiants CSI] Mercredi 20 janvier 2016 - Amphi 3

by Daniela Becker

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mercredi 20 janvier 2016 à partir de 10h30 en Amphi 3 (KB). -------------------------------------------- Au programme : VÉRIFICATION DU LOCUTEUR * 10h30 : La Segmentation du Locuteur Basée sur les Coefficients Cepstraux sur l’échelle de Mel – FANNY RIOLS La séparation du locuteur est un sujet important dans le domaine de la recherche. Il s’agit de savoir qui parle à quel moment dans un enregistrement audio, c’est-à-dire que nous aimerions connaître les intervalles de temps durant lesquels chaque locuteur parle. En calculant les Coefficients Cepstraux sur l’échelle de Mel (MFCC) de notre enregistrement audio, et en utilisant l’Analyse en Composantes Principales (ICA), nous pouvons avec l’aide de chaînes de Markov cachées (HMM), segmenter l’enregistrement. Nous utiliserons cet algorithme pour la segmentation du locuteur dans le système de vérification du locuteur, avec des enregistrements audio où plusieurs personnes parlent, comme dans les enregistrements d’entretiens ou bien les enregistrements microphone de l’évaluation de reconnaissance du locuteur de NIST. SPOT — BIBLIOTHÈQUE DE MODEL CHECKING * 11h00 : Améliorer la determinisation d’automates de Büchi – ALEXANDRE LEWKOWICZ L’algorithme de Safra permet de construire des automates de Rabin déterministes à partir d’automates de Büchi nondéterministes. Il existe une variante à cette méthode qui permet de construire des automates à parités déterministes. Cependant, ces méthodes produisent des automates avec 2O(n log n) états. Il existe des améliorations qui permettent de réduire le nombre d’états dans beaucoup de cas. Nous présentons deux nouvelles stratégies pour aider à réduire le nombre d’états final. La première stratégie utilise les composantes fortement connexes et utilise cette information pour suivre des chemins de Safra différents. La deuxième stratégie utilise l’information retournée par la bisimulation pour retirer des états équivalents. Ceci permet d’éviter de parcourir plusieurs chemins équivalents et ainsi de réduire le nombre d’états final. On montre que nos stratégies permettent souvent de construire des automates déterministes avec moins d’états et que ces automates reconnaissent toujours le même language. On donne des benchmarks pour voir le gain apporté par nos stratégies et on utilise un outil appelé ltl2dstar qui produit des automates de Rabin déterministes à partir de formules LTL pour comparer nos résultats. VCSN — BIBLIOTHÈQUE DE MANIPULATION D’AUTOMATES * 11h30 : Génération aléatoire d’automates et de chemins dans Vcsn – ANTOINE PIETRI Ce rapport présente l’implémentation d’une façon générique et performante pour générer des automates aléatoires pondérés. Pour ce faire, nous utilisons des relations déjà établies entre des ensembles connus et l’ensemble des DFA de taille n. En étendant ces relations dans le cas pondéré, nous généralisons l’algorithme présenté et nous montrons une implémentation dans la plateforme Vcsn. * 12h00 : Vcsn et la linguistique – SÉBASTIEN PIAT La théorie des automates étant utilisée pour représenter et manipuler des langages, la linguistique en est un des domaines d’application. La bibliothèque Vcsn n’a pas encore été utilisée pour de telles applications. La récente implémentation d’une méthode efficace de composition a rendu possible la création d’un traducteur utilisant des transducteurs. Nous présenterons les différentes étapes de l’implémentation d’un traducteur de language SMS ("bjr") vers le français ("bonjour") en utilisant Vcsn, et le pipeline du processus de traduction utilisant des automates. Nous verrons également les difficultés qu’a amenées son implémentation : de l’absence de certains algorithmes dans Vcsn aux mauvaises performances d’autres. * 12h30 : Composition Efficace de Transducteurs dans Vcsn – VALENTIN TOLMER Les transducteurs sont utilisés dans beaucoup de contextes, comme la reconnaissance de parole ou le calcul de la similitude entre protéines. Un des algorithmes fondamentaux pour les manipuler est la composition. Ce travail présente l’algorithme basique de composition, puis son extension à des transducteurs à transitions spontanées. Une adaptation paresseuse de l’algorithme est ensuite proposée, à la fois pour la composition et pour le pré-traitement (insplitting). Nous montrons ensuite que la version naïve de la composition variadique ne réduit pas la quantité de calculs nécessaires. Enfin, des mesures de performances comparent l’implémentation de la composition dans Vcsn à celle d’OpenFST. -- Daniela Becker Responsable administrative du LRDE

8 years, 11 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce January 2016