- Annonce

New journal publication: Model checking with generalized Rabin and Fin-less automata
by Alexandre Duret-Lutz 01 Apr '19

01 Apr '19

I'm happy to announce that the following journal article has been published in the International Journal on Software Tools for Technology Transfer Model checking with generalized Rabin and Fin-less automata Vincent Bloemen (1), Alexandre Duret-Lutz (2), Jaco van de Pol (3) (1) University of Twente, Enschede, The Netherlands (2) LRDE, EPITA, Kremlin-Bicêtre, France (3) University of Aarhus, Aarhus, Denmark https://www.lrde.epita.fr/wiki/Publications/bloemen.19.sttt 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 a transition-based generalized Rabin automaton (TGRA), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAshowever 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 and generated LTL formulas for models from the BEEM database. While we found little to no improvement by checking TGRAs directlywe show how various aspects of a TGRA's structure influences the model checking performance. In this paper, we also introduce a Fin-less acceptance condition, which is a disjunction of TGBAs. We show how to convert TGRAs into automata with Fin-less acceptance and show how a TGBA emptiness procedure can be extended to check Fin-less automata. -- Alexandre Duret-Lutz

1 0

Accepted Article at ELS2019
by lvalais 18 Mar '19

18 Mar '19

Greetings, I'm happy to announce that our paper, "Implementing Baker’s SUBTYPEP decision procedure", has been accepted to the 12th European Lisp Symposium, to be held in Genova on April 1-2 2019. The abstract is given below. Authors: Léo Valais, Jim Newton and Didier Verna We present here our partial implementation of Baker’s decision procedure for SUBTYPEP. In his article “A Decision Procedure for Common Lisp’s SUBTYPEP Predicate”, he claims to provide implementation guidelines to obtain a SUBTYPEP more accurate and as efficient as the average implementation. However, he did not provide any serious implementation and his description is sometimes obscure. In this paper we present our implementation of part of his procedure, only supporting primitive types, CLOS classes, member, range and logical type specifiers. We explain in our words our understanding of his procedure, with much more detail and examples than in Baker’s article. We therefore clarify many parts of his description and fill in some of its gaps or omissions. We also argue in favor and against some of his choices and present our alternative solutions. We further provide some proofs that might be missing in his article and some early efficiency results. We have not released any code yet but we plan to open source it as soon as it is presentable. Léo Valais

1 0

Paper accepted at ELS 2019
by Didier Verna 11 Mar '19

11 Mar '19

Greetings, I'm happy to report that my article entitled "Parallelizing Quickref" has been accepted to the 12th European Lisp Symposium, to be held in Genova on April 1-2 2019. The abstract is given below. I will also give a demo session of Quickref itself at the <Programming> conference. Quickref is a global documentation project for Common Lisp software. It builds a website containing reference manuals for Quicklisp libraries. Each library is first compiled, loaded, and introspected. From the collected information, a Texinfo file is generated, which is then processed into HTML. Because of the large number of libraries in Quicklisp, doing this sequentially may require several hours of processing. We report on our experiments parallelizing Quickref. Experimental data on the morphology of Quicklisp libraries has been collected. Based on this data, we are able to propose a number of parallelization schemes that reduce the total processing time by a factor of 3.8 to 4.5, depending on the exact situation. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Accepted Article at ELS2019
by Jim Newton 25 Feb '19

25 Feb '19

Greetings Colleagues, We are happy to announce that our paper, Finite Automata Theory Based Optimization of Conditional Variable Binding, has been accepted to the 2019 European Lisp Symposium, to be held in Genova Italy in April. Authors Jim Newton and Didier Verna The paper can be found here https://www.lrde.epita.fr/dload/papers/newton.19.els.pdf <https://www.lrde.epita.fr/dload/papers/newton.19.els.pdf> And the abstract is as follows: We present an efficient and highly optimized implementation of destructuring-case in Common Lisp. This macro allows the selection of the most appropriate destructuring lambda list of several given based on structure and types of data at run-time and thereafter dispatches to the corresponding code branch. We examine an optimization technique, based on finite automata theory applied to conditional variable binding and execution, and type-based pattern matching on Common Lisp sequences. A risk of inefficiency associated with a naive implementation of destructuring-case is that the candidate expression being examined may be traversed multiple times, once for each clause whose format fails to match, and finally once for the successful match. We have implemented destructuring-case in such a way to avoid multiple traversals of the candidate expression. This article explains how this optimization has been implemented. Happy reading Jim

1 0

[Seminaire-LRDE] Mercredi 6 mars 2019: Vincent Bismuth (GEHC)
by Edwin Carlinet 20 Feb '19

20 Feb '19

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 6 mars 2019 (11h -- 12h), Amphi 401. 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/2019-03-06 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 6 mars 2019 : * 11h -- 12h: Restauration de la vision grâce aux implants rétiniens -- Vincent Bismuth (GEHC) Rendre la vue à ceux qui l’ont perdue a longtemps été considéré comme un sujet réservé à la science-fiction. Cependant, sur les vingt dernières années les efforts intensifiés dans le domaine des prothèses visuelles ont abouti à des avancées significatives, et plusieurs centaines de patients dans le monde ont reçu de tels dispositifs. Ce séminaire présentera brièvement le domaine des prothèses rétiniennes avec une focalisation particulière sur les aspects de traitement d’image. Nous exposerons les principales approches, les limitations connues et les résultats. -- Vincent Bismuth mène une carrière dans le domaine du traitement d’images pour les dispositifs médicaux. Il a contribué pendant plus de dix ans aux développement d’algorithmes de traitement d’images et de vidéos pour les procédures chirurgicales interventionnelles chez GE Healthcare. Il s’est ensuite consacré pendant quatre ans à la conception de systèmes de restauration visuelle pour les malvoyants dans start-up Pixium Vision. Fin 2018, il a rejoint la division mammographie de GE Healthcare où il mène des développements en traitement d’images. 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. -- Edwin Carlinet Laboratoire R&D de l'EPITA (LRDE)

1 0

New publication: TACAS'19
by Ludovic Le Frioux 13 Feb '19

13 Feb '19

Greetings, We are pleased to announce that the following paper has been accepted in the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19). Please find the title and abstract below. Title and authors: "Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework" Ludovic Le Frioux (1,2) Souheib Baarir (1,2,3) Julien Sopena (2,4) Fabrice Kordon (2) (1) LRDE, EPITA, F-94043, Le Kremlin-Bicêtre (2) Sorbonne Université, CNRS, LIP6, UMR 7606, F-75005, Paris (3) Université Paris Lumières, Université Paris Nanterre, F-92000, Nanterre (4) Inria, DELYS Team, F-75005, Paris Abstract: Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First divide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. The second one portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances. An explanation resides on the difficulties to use the native formulation of the SAT problem (i.e., the CNF form) to compute an a priori good search space partitioning (i.e., all parallel solvers process their subspaces in comparable computational time). To avoid this, dynamic load balancing of the search subspaces is implemented. Unfortunately, this is difficult to compare load balancing strategies since state-of-the-art SAT solvers appropriately dealing with these aspects are hardly adaptable to various strategies than the ones they have been designed for. This paper aims at providing a way to overcome this problem by proposing an implementation and evaluation of different types of divide-and-conquer inspired from the literature. These are relying on the Painless framework, which provides concurrent facilities to elaborate such parallel SAT solvers. Comparison of the various strategies are then discussed. More information at: https://www.lrde.epita.fr/wiki/Publications/le-frioux.19.tacas

1 0

[Final CfP] 12th European Lisp Symposium, deadline extension
by Didier Verna 01 Feb '19

01 Feb '19

ELS'19 - 12th European Lisp Symposium Hotel Bristol Palace Genova, Italy April 1-2 2019 In cooperation with: ACM SIGPLAN In co-location with <Programming> 2019 Sponsored by EPITA and Franz Inc. http://www.european-lisp-symposium.org/ Recent news: - Submission deadline extended to Friday February 8. - Keynote abstracts now available. - <Programming> registration now open: https://2019.programming-conference.org/attending/Registration - Student refund program after the conference. 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 12th 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 Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following address: https://www.easychair.org/conferences/?conf=els2019 Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Important dates: - 08 Feb 2019 Submission deadline (*** extended! ***) - 01 Mar 2019 Notification of acceptance - 18 Mar 2019 Final papers due - 01-02 Apr 2019 Symposium Programme chair: Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Programme committee: Marco Antoniotti, Universita Milano Bicocca, Italy Marc Battyani, FractalConcept, France Pascal Costanza, IMEC, ExaScience Life Lab, Leuven, Belgium Leonie Dreschler-Fischer, University of Hamburg, Germany R. Matthew Emerson, thoughtstuff LLC, USA Marco Heisig, FAU, Erlangen-Nuremberg, Germany Charlotte Herzeel, IMEC, ExaScience Life Lab, Leuven, Belgium Pierre R. Mai, PMSF IT Consulting, Germany Breanndán Ó Nualláin, University of Amsterdam, Netherlands François-René Rideau, Google, USA Alberto Riva, Unversity of Florida, USA Alessio Stalla, ManyDesigns Srl, Italy Patrick Krusenotto, Deutsche Welle, Germany Philipp Marek, Austria Sacha Chua, Living an Awesome Life, Canada Search Keywords: #els2019, ELS 2019, ELS '19, European Lisp Symposium 2019, European Lisp Symposium '19, 12th ELS, 12th European Lisp Symposium, European Lisp Conference 2019, European Lisp Conference '19 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

Séminaire des étudiants chercheurs : Mercredi 16 janvier 2019 - Amphi IP11
by Daniela Becker 15 Jan '19

15 Jan '19

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mercredi 16 janvier 2019 à partir de 10h00 en Amphi IP11 (KB). Les étudiants ING3 présenteront le résultat de leurs travaux des derniers mois. Au programme : SPOT — BIBLIOTHEQUE DE MODEL CHECKING 10h00 Recherches de contrexemple dans Spot – CLÉMENT GILLARD Spot est une bibliothèque de manipulation d'ω-automates qui tend à aider la vérification de modèles par ω-automates et le développement d'outils de transformation d'ω-automates. Elle fournit donc de multiples algorithmes avec de multiples implémentations qui fonctionnent sur une grande variété d'ω-automates. Parmi ces algorithmes, les tests de vacuité et les recherches de contrexemple sont souvent utilisés pour diverses raisons. Comme leurs résultats sont liés, ils sont souvent utilisés ensemble. Cependant, il manque à Spot les implémentations de recherche de contrexemple correspondant à certaines implémentations de tests de vacuité qui soient capables de travailler de la même manière sur les mêmes automates. Nous présentons deux implémentations de calcul de contrexemple, qui viennent compléter deux implémentations de tests de vacuité déjà existantes, qui suivent leur sillage et se servent des données déjà accumulées pour construire efficacement des contrexemples. 10h30 Compression d’états dans Spot – ARTHUR REMAUD Pour représenter un système par un automate, il faut sauvegarder toutes les valeurs des variables du système pour chaque état de l'automate. Cela peut prendre beaucoup de place en mémoire lorsqu'il y a beaucoup de variables et/ou d'états, et de fait ralentit le temps d'exécution à cause des défauts de cache. Pour contourner ce problème dans Spot, on utilise une simple compression du tableau contenant les variables d'un état, et ce pour chaque état, ce qui réduit la mémoire utilisée et aussi le temps d'exécution. Dans ce rapport, nous présentons une structure de données qui améliore la compression des variables en utilisant la redondance des valeurs présentes dans différents états, et les différents problèmes rencontrés lors de son ajout dans Spot. 11h00 Mesures sur la réduction d’ordre partiel dans Spot – VINCENT TOURNEUR Ce rapport résume trois méthodes implémentées dans l'outil de vérification de modèles Spot. La première vise à améliorer la conversion de modèle de programme en structure de Kripke grâce à la réduction d'ordre partiel, une technique qui ignore l'ordre de certaines actions du programme. Cela permet de réduire la taille de la structure de Kripke. La seconde méthode modifie la première pour permettre de l'utiliser pour tester des propriétés LTL. La troisième a pour but de vérifier qu'un modèle ne contient pas de livelock, sans utiliser de propriété LTL. Nous testons toutes ces méthodes, en nous concentrant sur leur but commun : réduire la quantité de mémoire requise, ce qui est un goulot d'étranglement important dans le domaine de la vérification de modèles. -- Daniela Becker Responsable administrative du LRDE

1 0

[Reminder CfP] ELS 2019, 12th European Lisp Symposium, April 1-2, Genova
by Didier Verna 12 Jan '19

12 Jan '19

ELS'19 - 12th European Lisp Symposium Hotel Bristol Palace Genova, Italy April 1-2 2019 In cooperation with: ACM SIGPLAN In co-location with <Programming> 2019 Sponsored by EPITA http://www.european-lisp-symposium.org/ Recent news: - Keynote by Stefan Monnier on Emacs Lisp - Keynote by Christophe Rhodes on SBCL - Guest appearance by Matthew Flatt on Racket 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 12th 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 Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following address: https://www.easychair.org/conferences/?conf=els2019 Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Important dates: - 01 Feb 2019 Submission deadline - 01 Mar 2019 Notification of acceptance - 18 Mar 2019 Final papers due - 01-02 Apr 2019 Symposium Programme chair: Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Programme committee: Marco Antoniotti, Universita Milano Bicocca, Italy Marc Battyani, FractalConcept, France Pascal Costanza, IMEC, ExaScience Life Lab, Leuven, Belgium Leonie Dreschler-Fischer, University of Hamburg, Germany R. Matthew Emerson, thoughtstuff LLC, USA Marco Heisig, FAU, Erlangen-Nuremberg, Germany Charlotte Herzeel, IMEC, ExaScience Life Lab, Leuven, Belgium Pierre R. Mai, PMSF IT Consulting, Germany Breanndán Ó Nualláin, University of Amsterdam, Netherlands François-René Rideau, Google, USA Alberto Riva, Unversity of Florida, USA Alessio Stalla, ManyDesigns Srl, Italy Patrick Krusenotto, Deutsche Welle, Germany Philipp Marek, Austria Sacha Chua, Living an Awesome Life, Canada Search Keywords: #els2019, ELS 2019, ELS '19, European Lisp Symposium 2019, European Lisp Symposium '19, 12th ELS, 12th European Lisp Symposium, European Lisp Conference 2019, European Lisp Conference '19 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

FiXme 4.5 is released
by Didier Verna 03 Jan '19

03 Jan '19

Hello, I'm happy to announce the release of FiXme version 4.5. What's new in this version: * Public interface for extending FiXme with new key/value options. * Revamp the AUCTeX support * Fix PDF signature layouts not working anymore * Fix spurious space at the end of environments contents Grab it directly here: http://www.lrde.epita.fr/~didier/software/latex.php#fixme or wait until it propagates through CTAN... -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0