Annonce

annonce@lrde.epita.fr

564 discussions

Paper accepted at ELS 2019

by Didier Verna

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

6 years

Accepted Article at ELS2019

by Jim Newton

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

6 years, 1 month

[Seminaire-LRDE] Mercredi 6 mars 2019: Vincent Bismuth (GEHC)

by Edwin Carlinet

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)

6 years, 1 month

New publication: TACAS'19

by Ludovic Le Frioux

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

6 years, 1 month

[Final CfP] 12th European Lisp Symposium, deadline extension

by Didier Verna

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

6 years, 2 months

Séminaire des étudiants chercheurs : Mercredi 16 janvier 2019 - Amphi IP11

by Daniela Becker

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

6 years, 2 months

[Reminder CfP] ELS 2019, 12th European Lisp Symposium, April 1-2, Genova

by Didier Verna

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

6 years, 2 months

FiXme 4.5 is released

by Didier Verna

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

6 years, 2 months

Spot 2.7 released

by Alexandre Duret-Lutz

We are happy to announce the release of Spot 2.7 This release contains contributions by Maximilien Colange, Etienne Renault, and myself. See below for a detailed list of new features. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.7.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.7 (2018-12-11) Command-line tools: - ltlsynt now has three algorithms for synthesis: --algo=sd is the historical one. The automaton of the formula is split to separate inputs and outputs, then determinized (with Safra construction). --algo=ds the automaton of the formula is determinized (Safra), then split to separate inputs and outputs. --algo=lar translate the formula to a deterministic automaton with an arbitrary acceptance condition, then turn it into a parity automaton using LAR, and split it. In all three cases, the obtained parity game is solved using Zielonka algorithm. Calude's quasi-polynomial time algorithm has been dropped as it was not used. - ltlfilt learned --liveness to match formulas representing liveness properties. - the --stats= option of tools producing automata learned how to tell if an automaton uses universal branching (%u), or more precisely how many states (%[s]u) or edges (%[e]u) use universal branching. Python: - spot.translate() and spot.postprocess() now take an xargs= argument similar to the -x option of ltl2tgba and autfilt, making it easier to fine tune these operations. For instance ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0 would be written in Python as spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') (Note: those extra options are documented in the spot-x(7) man page.) - spot.is_generalized_rabin() and spot.is_generalized_streett() now return a tuple (b, v) where b is a Boolean, and v is the vector of the sizes of each generalized pair. This is a backward incompatible change. Library: - The LTL parser learned syntactic sugar for nested ranges of X using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These correspond to the next!, next_e!, and next_a! operators of PSL, but we do not support those under these names currently.) X[6]a = XXXXXXa F[2:4]a = XX(a | X(a | Xa)) G[2:4]a = XX(a & X(a & Xa)) The corresponding constructors (for C++ and Python) are formula::X(unsigned, formula) formula::F(unsigned, unsigned, formula) formula::G(unsigned, unsigned, formula) - spot::unabbreviate(), used to rewrite away operators such as M or W, learned to use some shorter rewritings when an argument (e) is a pure eventuality or (u) is purely universal: Fe = e Gu = u f R u = u f M e = F(f & e) f W u = G(f | u) - The twa_graph class has a new dump_storage_as_dot() method to show its data structure. This is more conveniently used as aut.show_storage() in a Jupyter notebook. See https://spot.lrde.epita.fr/ipynb/twagraph-internals.html - spot::generic_emptiness_check() is a new function that performs emptiness checks of twa_graph_ptr (i.e., automata not built on-the-fly) with an *arbitrary* acceptance condition. Its sister spot::generic_emptiness_check_scc() can be used to decide the emptiness of an SCC. This is now used by twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and scc_info::determine_unknown_acceptance(). - The new function spot::to_parity() translates an automaton with arbitrary acceptance condition into a parity automaton, based on a last-appearance record (LAR) construction. (It is used by ltlsynt but not yet by autfilt or ltl2tgba.) - The new function is_liveness() and is_liveness_automaton() can be used to check whether a formula or an automaton represents a liveness property. - Two new functions count_univbranch_states() and count_univbranch_edges() can help measuring the amount of universal branching in alternating automata. Bugs fixed: - translate() would incorrectly mark as stutter-invariant some automata produced from formulas of the form X(f...) where f... is syntactically stutter-invariant. - acc_cond::is_generalized_rabin() and acc_cond::is_generalized_streett() did not recognize the cases were a single generalized pair is used. - The pair of acc_cond::mark_t returned by acc_code::used_inf_fin_sets(), and the pair (bool, vector_rs_pairs) by acc_cond::is_rabin_like() and acc_cond::is_streett_like() were not usable in Python. - Many object types had __repr__() methods that would return the same string as __str__(), contrary to Python usage where repr(x) should try to show how to rebuild x. The following types have been changed to follow this convention: spot.acc_code spot.acc_cond spot.atomic_prop_set spot.formula spot.mark_t spot.twa_run (__repr__ shows type and address) spot.twa_word (likewise, but _repr_latex_ used in notebooks) Note that this you were relying on the fact that Jupyter calls repr() to display returned values, you may want to call print() explicitely if you prefer the old representation. - Fix compilation under Cygwin and Alpine Linux, both choking on undefined secure_getenv().

6 years, 3 months

[Seminaire-LRDE] Vendredi 14 décembre 2018: Clara Jaquet (ESIEE Marne-la-Vallée)

by Edwin Carlinet

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 Vendredi 14 décembre 2018 (11h--12h), Amphi IP12A. 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/2018-12-14 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Vendredi 14 décembre 2018 : * 11h--12h: Toward myocardium perfusion from X-ray CT -- Clara Jaquet (ESIEE Marne-la-Vallée) Recent advances in medical image computing have resulted in automated systems that closely assist physicians in patient therapy. Computational and personalized patient models benefit diagnosis, prognosis and treatment planning, with a decreased risk for the patient, as well as potentially lower cost. HeartFlow Inc. is a successful example of a company providing such a service in the cardiovascular context. Based on patient-specific vascular model extracted from X-ray CT images, they identify functionally significant disease in large coronary arteries. Their combined anatomical and functional analysis is nonetheless limited by the image resolution. At the downstream scale, a functional exam called Myocardium Perfusion Imaging (MPI) highlights myocardium regions with blood flow deficit. However, MPI does not functionally relate perfusion to the upstream coronary disease. The goal of our project is to build the functional bridge between coronary and myocardium. To this aim we propose an anatomical and functional extrapolation. We produce an innovative vascular network generation method extending the coronary model down to the microvasculature. In the resulting vascular model, we compute a functional analysis pipeline to simulate flow from large coronaries to the myocardium, and to enable comparison with MPI ground-truth data. -- After completing a technological university degree in biology at Creteil, Clara Jaquet obtained the diploma of biomedical engineer from ISBS (Bio-Sciences Institute) in 2015. She worked for one year at HeartFlow Inc, California, before starting a PhD at ESIEE, Université Paris-Est, within the LIGM laboratory, on a research project jointly with the same company. 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) _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

6 years, 3 months

← Newer
1
...
7
8
9
10
11
12
13
...
57
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce