Annonce

annonce@lrde.epita.fr

543 discussions

Séminaire des étudiants chercheurs du LRDE : Mardi 2 juillet 2019 à 13h - Amphi 2

by Daniela Becker

Bonjour, Nous avons le plaisir de vous inviter au Séminaire des étudiants chercheurs du LRDE. Ils présenteront le résultat de leurs travaux le mardi 2 juillet en amphi 2 à partir de 13h. Au programme : - Climb : 13h00 : Antoine Hacquard "Parallélisation et Indexation de Quickref" - Oléna : 13h30 : Thibault Buatois "Segmentation de tumeur cérébrale par réseau de neurones convolutionnel" 14h00 : Célian Gossec "Création d'un lien entre une bibliothèque de traitement d'images en C++ haute performance vers Python" 14h30 Pause - Spot : 14h45 : Samuel Corno "Utilisation du Scatter Search pour trouver un meilleur ordre de variable dans les BDD" 15h15 : Paul Guénézan "Exploration d'espace d'états distribuée" 15h45 : Martin Huvelle "Réimplémentation des automates testeurs dans Spot" 16h15 : Antoine Martin "Comment implémenter le support des goroutines dans go2pins" Pour plus d’informations, voir ici : https://www.lrde.epita.fr/wiki/Student_Seminar_2019-07-02 L'entrée du séminaire est libre. -- Daniela Becker Responsable administrative du LRDE

4 years, 10 months

Soutenance de thèse de Ludovic Le Frioux

by Ludovic Le Frioux

Bonjour à tous, J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée : "Vers une parallélisation efficace de la résolution du problème de satisfaisabilité" L'exposé se déroulera en français. Vous êtes également cordialement invité au pot qui suivra. Date : le mercredi 3 juillet à 14h Lieu : en salle KB604 à l'EPITA, 14-16 rue Voltaire, Le Kremlin-Bicêtre 94270 Vous trouverez également toutes les informations sur la page web suivante : https://www.lrde.epita.fr/wiki/Affiche-these-LLF Le jury sera composé de : Rapporteurs: * Michaël KRAJECKI, Professeur à l'Université de Reims, CReSTIC * Laurent SIMON, Professeur à l'Université de Bordeaux, LaBRI, CNRS Examinateurs: * Daniel LE BERRE, Professeur à l'Université d'Artois, CRIL, CNRS * Bertrand LE CUN, Ingénieur Senior à Google Inc. * Clémence MAGNIEN, Directeur de Recherche au CNRS, LIP6, CNRS Encadrants: * Souheib BAARIR, Maître de Conférence à l'Université Paris Nanterre, LIP6, CNRS * Fabrice KORDON, Professeur à Sorbonne Université, LIP6, CNRS * Julien SOPENA, Maître de Conférence à Sorbonne Université, LIP6, CNRS, INRIA Mots clés : satisfaisabilité booléenne, parallélisation, portfolio, diviser pour régner, échange de clauses, outil Le résumé de la thèse est le suivant : Les solveurs résolvants le problème de SATisfiabilité booléenne sont utilisés avec succès dans de nombreux contextes : vérification de programmes et de matériels, cryptographie, bio-informatique, preuve automatique de théorème, etc. Ceci est dû à leur capacité à résoudre d'énormes problèmes pouvant contenir des millions de variables et des dizaines de millions de contraintes. Alors que la plupart des solveurs SAT ont longtemps été séquentiels, l'émergence des machines multi-cœurs a ouvert de nouvelles perspectives dans ce domaine. Il existe de nombreux solveurs SAT parallèles différents par leurs stratégies, langages de programmation, bibliothèques utilisées, etc. Il est donc difficile de comparer l'efficacité de différentes stratégies dans un cadre unifié et équitable. De plus, l'introduction de nouvelles approches nécessite une compréhension approfondie de l'implémentation des solveurs déjà existants. Cette thèse présente Painless : une plateforme générique et modulaire permettant l'implémentation de solveurs SAT parallèles efficaces pour les machines multi-cœurs. Elle offre une implémentation des composants de base et sa modularité permet aux utilisateurs de créer facilement leurs solveurs parallèles basés sur de (nouvelles) stratégies. Painless a permis de construire et tester de nombreux solveurs. Nous avons pu imiter le comportement de trois solveurs de l'état de l'art tout en factorisant de nombreuses parties du code. L'efficacité de Painless a été soulignée par le fait que ces implémentations sont au moins aussi efficaces que les originales. De plus, lors de la participation à la compétition annuelle internationale de solveurs SAT parallèles, l'un de nos solveurs s'est classé 3ème en 2017 et un autre 1er en 2018. Nous avons utilisé Painless pour mener des expériences équitables avec des solveurs de type diviser pour régner. Celles-ci nous ont permis de mettre en lumière des compositions originales d'heuristiques plus performantes que celles déjà présentes dans l’état de l’art. Enfin nous avons été en mesure de créer et tester de nouvelles stratégies exploitant la structure modulaire des formules SAT. L'approche que nous avons proposée utilise la topologie de la formule pour guider le solveur vers des zones plus riches en informations, permettant ainsi l’accélération de la résolution parallèle du problème. A bientôt, Ludovic LE FRIOUX

4 years, 10 months

Séminaire des étudiants chercheurs RDI : Lundi 1er juillet 2019 à 13h - Amphi Master

by Daniela Becker

Bonjour, Nous avons le plaisir de vous inviter au Séminaire des étudiants de la majeure double compétence recherche (RDI) composée d'étudiants venant aussi bien du LRDE que du LSE. Il se déroulera le 1er juillet en amphi master à partir de 13h. Les sujets abordés sont : 13h00 : « Modeling and Identifying Troll Farm Accounts on Twitter » - Antoine Sainson (LSE) 13h30 : « Automatic troll farm detection on Twitter » - Hugo Linsenmaier (LSE) 14h00 : « Génération d'états artificiels dans des espaces d'états à l'aide d'estimations de densité paramétriques et non paramétriques. » - Thomas de Carvalho (LRDE) 14h30 : « Estimation de la fonction de niveau de bruit à l'aide de l'arbre des formes dans des images naturelles » - Baptiste Esteban (LRDE) 15h15 : « Génération d'images marines réalistes » - Charles Ginane (LRDE) 15h45 : « Integrating Mathematical Morphology with Deep Convolutional Neural Networks » - Alexandre Kirszenberg (LRDE) 16h15 : « Introduction des opérateurs morphologiques dans les réseaux de neurones convolutionels profonds » - Younes Koudhli (LRDE) 16h45 : « An implementation of Baker’s SUBTYPEP decision procedure » - Léo Valais (LRDE) Pour plus d’informations, voir ici : https://www.lrde.epita.fr/wiki/Student_Seminar_2019-07-01 L'entrée du séminaire est libre. -- Daniela Becker Responsable administrative du LRDE

4 years, 10 months

Programme du Séminaire MeFoSyLoMa du 24 mai 2019 à l'Epita

by Alexandre Duret-Lutz

======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/ Méthodes Formelles pour les Systèmes Logiciels et Matériels vendredi 24 mai 2019, 14h-16h30 Adresse: Amphi 3 14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : https://www.google.com/maps/place/14+Rue+Voltaire,+94270+Le+Kremlin-Bicêtre/ https://www.lrde.epita.fr/~adl/dl/acces-amphi3.png S'il y en a parmi vous qui comptent venir en voiture, le parking du centre commercial Okabé est gratuit pendant 3h. http://www.okabe.com/okabe/fr/okabe-parking ======================================================================== Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC), LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la confrontation de différentes approches ou points de vue sur l'utilisation des méthodes formelles dans les domaines du génie logiciel, de la conception de circuit, des systèmes répartis, des systèmes temps-réel ou encore des systèmes d'information. Il s'organise autour de réunions bimestrielles où sont exposés des travaux de recherche récents sur ce thème. ======================================================================== Programme 14h00-14h45: Benoît Barbot (LACL) Generation of Signals under Temporal Constraints for CPS Testing This work is concerned with validation of cyber-physical systems (CPS) via simulation based on sampling of the input signal space. Such a space is infinite and in general too difficult to treat symbolically meaning that the only reasonable option is to sample a finite subset of it and simulate the corresponding system behaviours. It is thus of great interest to choose a finite sample so that it best "covers" the whole space of input signals. We use timed automata to model temporal constraints, in order to avoid spurious bugs coming from unrealistic inputs and this can also reduce the input space to explore. We propose a method for low discrepancy generation of signals with temporal constraints recognised by timed automata. The discrepancy notion reflects how uniform the input signal space is sampled and additionally allows deriving validation and performance guarantees. We also show how this notion can be used to measure the discrepancy of a given set of input signals. We describe a prototype tool chain and demonstrate the proposed methods on a Kinetic Battery Model (KiBaM) and a Sigma Delta modulator. 14h45-15h30 : Alexandre Duret-Lutz (LRDE) Generic Emptiness Check for Fun and Profit Abstract: We present a new algorithm for checking the emptiness of ω-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions. Joint work with C. Baier, F. Blahoudek, J. Klein, D. Müller, and J. Strejček. 15h30-16h00: pause café 16h00-16h30: vie du groupe ======================================================================== -- Alexandre Duret-Lutz

4 years, 11 months

New publication at TUG 2019

by Didier Verna

Hello, I'm happy to announce the acceptance of a new publication for TUG 2019 (the TeX users group conference) to be held in Palo Alto, CA, USA, next August. See below for the title and abstract: Quickref: a Stress Test for Texinfo Quickref is a global documentation project for the Common Lisp ecosystem. It creates reference manuals automatically by introspecting libraries and generating a corresponding documentation in Texinfo format. The Texinfo files may subsequently be converted into PDF or HTML. Quickref is non-intrusive: software developers do not have anything to do to get their libraries documented by the system. Quickref may be used to create a local website documenting your current, partial, working environment, but it is also able to document the whole Common Lisp ecosystem at once. The result is a website containing almost two thousand reference manuals. Quickref provides a Docker image for an easy recreation of this website, but a public version is also available and kept up to date on quickref.common-lisp.net. Quickref constitutes an enormous (and successful) stress test for Texinfo, and not only because of the number of files generated and processed. The Texinfo file sizes range from 7K to 15M (make it double for the generated HTML ones). The number of lines of Texinfo code in those files extend from 364 to 285,020, the indexes may contain between 14 and 44500 entries, and the processing times vary from .3s to 1m 38s per file. In this paper, we give an overview of the design and architecture of the system, describe the challenges and difficulties in generating valid Texinfo code automatically, and put some emphasis on the currently remaining problems and deficiencies. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

5 years

Quickref 2.0 is released

by Didier Verna

I'm happy to announce the release of Quickref 2.0, codename "Be Quick or Be Dead". Quickref is a global documentation project for Common Lisp libraries, currently offering 1720 reference manuals on the official website: http://quickref.common-lisp.net. Quickref can also be run locally, either from the provided Docker image, or directly from the Lisp REPL. This release is appropriately named after its most important new feature: a support for parallelism which has been presented last week at ELS 2019, the 12th European Lisp Symposium. In addition to that, we also have a new, author based, index to the provided manuals, and a continuous integration infrastructure for keeping track of new Quicklisp (or Quickref) releases more easily. Thanks to Antoine Hacquard, Antoine Martin, and Erik Huelsmann for their contribution to this version! -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

5 years

[Seminaire-LRDE] Mercredi 10 avril 2019: Guillaume Charpiat (TAU-team, INRIA Saclay / LRI - Université Paris-Sud)

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 10 avril 2019 (11h -- 12h), Amphi 4. 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-04-10 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 10 avril 2019 : * 11h -- 12h: Deep Learning for Satellite Imagery: Semantic Segmentation, Non-Rigid Alignment, and Self-Denoising -- Guillaume Charpiat (TAU-team, INRIA Saclay / LRI - Université Paris-Sud) https://www.lri.fr/~gcharpia/ Neural networks have been producing impressive results in computer vision these last years, in image classification or segmentation in particular. To be transferred to remote sensing, this tool needs adaptation to its specifics: large images, many small objects per image, keeping high-resolution output, unreliable ground truth (usually mis-registered). We will review the work done in our group for remote sensing semantic segmentation, explaining the evolution of our neural net architecture design to face these challenges, and finally training a network to register binary cadaster maps to RGB images while detecting new buildings if any, in a multi-scale approach. We will show in particular that it is possible to train on noisy datasets, and to make predictions at an accuracy much better than the variance of the original noise. To explain this phenomenon, we build theoretical tools to express input similarity from the neural network point of view, and use them to quantify data redundancy and associated expected denoising effects. If time permits, we might also present work on hurricane track forecast from reanalysis data (2-3D coverage of the Earth's surface with temperature/pressure/etc. fields) using deep learning. -- After a PhD thesis at ENS on shape statistics for image segmentation, and a year in Bernhard Schölkopf's team at MPI Tübingen on kernel methods for medical imaging, Guillaume Charpiat joined INRIA Sophia-Antipolis to work on computer vision, and later INRIA Saclay to work on machine learning. Lately, he has been focusing on deep learning, with in particular remote sensing imagery as an application field. 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

5 years, 1 month

New journal publication: Model checking with generalized Rabin and Fin-less automata

by Alexandre Duret-Lutz

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

5 years, 1 month

Accepted Article at ELS2019

by lvalais

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

5 years, 1 month

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

5 years, 1 month

← Newer
1
...
4
5
6
7
8
9
10
...
55
Older →

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce