Annonce

annonce@lrde.epita.fr

1 participants
563 discussions

[Seminaire-LRDE] Mercredi 17 décembre 2014: Christian Queinnec, UPMC, LIP6

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 17 décembre 2014 (11h00--12h00), 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/2014-12-17 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 17 décembre 2014 : * 11h: D’un MOOC à l'autre -- Christian Queinnec, UPMC, LIP6 http://lip6.fr/Christian.Queinnec/ Au printemps 2014, j'ai animé un MOOC d'initiation à l'informatique, centré sur la programmation récursive. Bien que loin d'être massif, ce MOOC a permis d'expérimenter ce nouveau medium ainsi que de mettre à l'épreuve une infrastructure de correction automatisée. L'exposé portera sur ces deux aspects et présentera également les nouveautés prévues pour la prochaine édition de ce MOOC. -- Lispeur depuis 1974, Unixien depuis 1984, HDR depuis 1988, et depuis peu professeur émérite de l’UPMC. Surtout connu pour ses livres sur Lisp et Scheme, il a récemment animé le MOOC ``Programmation Récursive'' dont il sera question dans l’exposé. 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

10 years

exposé de Maximilien Collenge sur des automates de Büchi avec compteurs le 4 décembre au LRDE

by Alexandre Duret-Lutz

Le 4 décembre, à 14h, au LRDE (https://www.lrde.epita.fr/wiki/Contact), Maximilien Collenge, actuellement en post-doc à l'université de Genève, fera un exposé sur les automates de Büchi avec compteurs. Abstract: Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties. When the quantitative domain is discrete, quantities can be encoded as automata states, and quantitative model-checking is thus reduced to qualitative model-checking. To this end, the initial model is enhanced with new state variables that keep track of the observed quantities, while the quantitative property is rephrased as a qualitative one over the enhanced model. However, such a quantitative-to-qualitative approach lacks generality and is prone to errors, as it makes no clear distinction between the system to be verified (the actual behavior) and the property to be checked (the desired behavior). We propose a cleaner method for discrete quantitative model-checking by extending linear temporal logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This extension can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. -- Alexandre Duret-Lutz

10 years

Soutenance de thèse de E. Renault

by Etienne Renault

Bonjour, J'ai le plaisir de vous convier à ma soutenance de thèse qui aura lieu le Vendredi 5 Décembre 2014 à 14h en salle salle 211 - tour 55 - couloir 55/65 - 2ème étage. La soutenance sera suivie d’un pot. Sujet de la thèse : « Contribution aux tests de vacuité pour le model checking explicite » Membre du jury : Laure. Petrucci (Professeur à l’Université Paris 13): rapporteur Francois Vernadat (Professeur à l’INSA toulouse): rapporteur Jean-Michel. Couvreur (Professeur à l’Université d’Orléans) : examinateur Emmanuelle Encrenaz (Maitre de conférence à l’Université Paris 6): examinateur Jaco van de Pol (Professeur à l’Université de Twente): examinateur Alexandre Duret-Lutz (Maitre de conférence à l’EPITA): encadrant de thèse D. Poitrenaud (Maitre de conférence à l’Université Paris 6): encadrant de thèse Fabrice Kordon (Professeur à l’Université Paris 6): Directeur de thèse Plan d’accès : http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.… Résumé : ———— L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d’omega-automates reconnaissant des mots infinis. Des manipulations de ces automates (produit synchronisé et test de vacuité) permettent d'établir si le système vérifie la propriété ou non. Dans cette thèse nous nous focalisons sur un type particulier d'omega-automates qui permettent une représentation concise des propriétés d'équité faible: les automates de Büchi généralisés basés sur les transitions (TGBA ou Transition-based Generalized Büchi Automata). Dans un premier temps, nous brossons un aperçu des algorithmes de vérification existant et nous en proposons de nouveaux traitant efficacement les automates généralisés forts. Dans un second temps, l'analyse des composantes fortement connexes de l'automate de la propriété nous a conduit à élaborer une décomposition de cet automate. Cette décomposition se focalise sur les automates multi-forces et permet une parallélisation naturelle des model-checkers. Enfin, nous avons proposé les premiers tests de vacuité parallèles pour les automates généralisés. De plus, tous ces tests sont lock-free à la différence de ceux de l’état de l’art. Toutes ces techniques ont ensuite été implémentées et évaluées sur un jeu de test conséquent. Abstract : ———— The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA). First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first time, new parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.

10 years, 1 month

[Seminaire-LRDE] Demain, Mercredi 19 novembre 2014 : Markus Voelter, independent/itemis

by Daniela Becker

Bonjour, petit rappel : la prochaine séance du Séminaire du LRDE aura lieu demain, Mercredi 19 novembre 2014 (11h30--13h), en Amphi 1. Au programme : * 11h30: Generic Tools, Specific Languages -- Markus Voelter, independent/itemis http://www.voelter.de Generic Tools, Specific Languages is an approach for developing tools and applications in a way that supports easier and more meaningful adaptation to specific domains. To achieve this goal, GTSL generalizes programming language IDEs to domains traditionally not addressed by languages and IDEs. At its core, GTSL represents applications as documents / programs / models expressed with suitable languages. Application functionality is provided through an IDE that is aware of the languages and their semantics. The IDE provides editing support, and also directly integrates domain-specific analyses and execution services. Applications and their languages can be adapted to increasingly specific domains using language engineering; this includes developing incremental extensions to existing languages or creating additional, tightly integrated languages. Language workbenches act as the foundation on which such applications are built. -- Dr. Markus Voelter works as an independent researcher, consultant and coach for itemis AG in Stuttgart, Germany. His focus is on software architecture, model-driven software development and domain specific languages as well as on product line engineering. Markus also regularly writes (articles, patterns, books) and speaks (trainings, conferences) on those subjects. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

10 years, 1 month

[Seminaire-LRDE] Mercredi 19 novembre 2014: Markus Voelter, independent/itemis

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 19 novembre 2014 (11h30--13h), Amphi 1. 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/2014-11-19 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 19 novembre 2014 : * 11h30: Generic Tools, Specific Languages -- Markus Voelter, independent/itemis http://www.voelter.de Generic Tools, Specific Languages is an approach for developing tools and applications in a way that supports easier and more meaningful adaptation to specific domains. To achieve this goal, GTSL generalizes programming language IDEs to domains traditionally not addressed by languages and IDEs. At its core, GTSL represents applications as documents / programs / models expressed with suitable languages. Application functionality is provided through an IDE that is aware of the languages and their semantics. The IDE provides editing support, and also directly integrates domain-specific analyses and execution services. Applications and their languages can be adapted to increasingly specific domains using language engineering; this includes developing incremental extensions to existing languages or creating additional, tightly integrated languages. Language workbenches act as the foundation on which such applications are built. -- Dr. Markus Voelter works as an independent researcher, consultant and coach for itemis AG in Stuttgart, Germany. His focus is on software architecture, model-driven software development and domain specific languages as well as on product line engineering. Markus also regularly writes (articles, patterns, books) and speaks (trainings, conferences) on those subjects. 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

10 years, 1 month

[these] Soutenance : Florian Lesaint, 26 septembre 2014, ISIR - Paris

by Florian Lesaint

Bonjour, J'ai le plaisir de vous inviter à ma soutenance de thèse, intitulée *Modélisation du conditionnement animal par représentations factorisées dans un système d'apprentissage dual : Explication des différences inter-individuelles aux niveaux comportemental et neurophysiologique* qui aura lieu le vendredi 26 septembre 2014 à 14h, à l'ISIR, UPMC/CNRS, 4 Place Jussieu, Paris Tour 65, 3ème étage, couloir 65-66, salle 304. (plan: http://www.isir.upmc.fr/UserFiles/Image/plan-sout-thesis-lesaint.png) Membres du jury: M. Angelo Arleo -- Directeur de recherche CNRS - INSERM - Université Pierre et Marie Curie -- Examinateur M. Etienne Coutureau -- Chargé de recherche CNRS à l'Université de Bordeaux -- Rapporteur M. Peter Dayan -- Professor at University College London -- Examinateur M. Arthur Leblois -- Chargé de recherche CNRS à l'Université Paris Descartes -- Rapporteur M. Mehdi Khamassi -- Chargé de recherche CNRS à l'Université Pierre et Marie Curie -- Co-encadrant M. Olivier Sigaud -- Professeur de l'Université Pierre et Marie Curie -- Directeur de thèse Un résumé des travaux présentés figure en fin de ce message. La soutenance se déroulera en anglais. Vous êtes chaleureusement conviés au pot qui suivra la soutenance dans le hall de l'ISIR. Amicalement, Florian Lesaint ** FR ********************************************************************* Résumé: Le conditionnement Pavlovien, l'acquisition de réponses vers des stimuli neutres associés à des récompenses, et le conditionnement instrumental, l'expression de comportements pour atteindre des buts, sont au cœur de nos capacités d'apprentissage. Ils sont souvent étudiés séparément malgré les preuves de leur enchevêtrement. Les modèles de conditionnement instrumental reposent sur le formalisme de l'apprentissage par renforcement (RL), alors que les modèles du conditionnement Pavlovien reposent surtout sur des architectures dédiées souvent incompatibles avec ce formalisme, compliquant l'étude de leurs interactions. Notre objectif est de trouver des concepts, qui combinés à des modèles RL puissent offrir une architecture unifiée permettant une telle étude. Nous développons un modèle qui combine un système RL classique, qui apprend une valeur par état, avec un système RL révisé, évaluant les stimuli séparément et biaisant le comportement vers ceux associés aux récompenses. Le modèle explique certaines réponses inadaptées par l'interaction néfaste des systèmes, ainsi que certaines différences inter-individuelles par une simple variation au niveau de la population de la contribution de chaque système dans le comportement global. Il explique une activité inattendue de la dopamine, vis-à-vis de l'hypothèse qu'elle encode un signal d'erreur, par son calcul sur les stimuli et non les états. Il est aussi compatible avec une hypothèse alternative que la dopamine contribue aussi à rendre certains stimuli recherchés pour eux-mêmes. Le modèle présente des propriétés prometteuses pour l'étude du conditionnement Pavlovien, du conditionnement instrumental et de leurs interactions. ** EN ********************************************************************* Title: Modelling animal conditioning with factored representations in dual-learning systems: Explaining inter-individual differences at behavioural and neurophysiological levels Summary: Pavlovian conditioning, the acquisition of responses to neutral stimuli previously paired with rewards, and instrumental conditioning, the acquisition of goal-oriented responses, are central to our learning capacities. However, despite some evidences of entanglement, they are mainly studied separately. Reinforcement learning (RL), learning by trials and errors to reach goals, is central to models of instrumental conditioning, while models of Pavlovian conditioning rely on more dedicated and often incompatible architectures. This complicates the study of their interactions. We aim at finding concepts which combined with RL models may provide a unifying architecture to allow such a study. We develop a model that combines a classical RL system, learning values over states, with a revised RL system, learning values over individual stimuli and biasing the behaviour towards reward-related ones. It explains maladaptive behaviours in pigeons by the detrimental interaction of systems, and inter-individual differences in rats by a simple variation at the population level in the contribution of each system to the overall behaviour. It explains unexpected dopaminergic patterns with regard to the dominant hypothesis that dopamine parallels a reward prediction error signal by computing such signal over features rather than states, and makes it compatible with an alternative hypothesis that dopamine also contributes to the acquisition of incentive salience, making reward-related stimuli wanted for themselves. The present model shows promising properties for the investigation of Pavlovian conditioning, instrumental conditioning and their interactions. -- Florian LESAINT Institut des Systèmes Intelligents et de Robotique (UMR7222) CNRS - Université Pierre et Marie Curie Pyramide, Tour 55 - Boîte courrier 173 4 place Jussieu, 75252 Paris Cedex 05, France http://www.isir.upmc.fr

10 years, 3 months

L'air de rien 32.0

by Daniela Becker

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°32 du bulletin du LRDE. C'est un numéro Spécial Rentrée qui présente l'ensemble des permanents du LRDE. Vous y trouverez également un aperçu des activités du LRDE et de la majeure CSI dont font partie tous les élèves épitéens intégrant le labo. Vous pouvez télécharger le bulletin en couleur à la page suivante : https://www.lrde.epita.fr/wiki/Latest_issue -- Daniela Becker Responsable administrative du LRDE

10 years, 3 months

Soutenance de thèse d'Ala Eddine BEN SALEM 25 Septembre 2014, 14h, bâtiment 41, salle 203-LIP6

by ala-eddine.ben-salem

Bonjour, J'ai le plaisir de vous inviter à ma soutenance de thèse intitulée "Improving the Model Checking of Stutter-Invariant LTL Properties". Elle aura lieu au Laboratoire d'Informatique de Paris 6 (LIP6) à Jussieu, le **jeudi 25 Septembre 2014 à 14h00 en salle 203, bâtiment 41** et vous êtes également chaleureusement conviés au pot qui suivra. Plan d'accès : http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.… Cordialement, Ala Eddine BEN SALEM ---------------------------------------------------------------- Jury ---------------------------------------------------------------- M. Radu Mateescu (INRIA), Rapporteur M. Stefan Schwoon (ENS Cachan), Rapporteur Mme. Béatrice BÉRARD (UPMC, Paris 6), Examinateur M. Didier BUCHS (Université de Genève), Examinateur M. Fabrice Kordon (UPMC, Paris 6), Directeur de thèse M. Alexandre Duret-Lutz (EPITA), Encadrant ---------------------------------------------------------------- Résumé de la thèse ---------------------------------------------------------------- Les systèmes logiciels sont devenus omniprésents se substituant à l’homme pour des tâches délicates, souvent critiques, mettant en jeu des coûts importants voire des vies humaines. Les conséquences des défaillances imposent la recherche de méthodes rigoureuses pour la validation des systèmes. L’approche par automates du model-checking est la plus classique des approches de vérification automatique. Elle prend en entrée un modèle du système et une propriété, et permet de savoir si cette dernière est vérifiée. Pour cela un model-checker traduit la négation de la propriété en un automate et vérifie si le produit du système et de cet automate est vide. Hélas, bien qu’automatique, cette approche souffre d'une explosion combinatoire du nombre d’états du produit obtenu. Afin de combattre ce problème, en particulier lors de la vérification des propriétés insensibles au bégaiement, nous proposons la première évaluation d’automates testeur (TA) sur des modèles réalistes, une amélioration de l’algorithme de vérification pour ces automates et une méthode permettant de transformer un TA en un automate (STA) permettant une vérification en une seule passe. Nous proposons aussi une nouvelle classe d’automates: les TGTA. Ces automates permettent une vérification en une seule passe sans ajouter d’états artificiels. Cette classe combine les avantages des TA et des TGBA (automates de Büchi). Les TGTA permettent d’améliorer les approches explicite et symbolique de model-checking. Notamment, en combinant les TGTA avec la technique de saturation, les performances de l'approche symbolique sont améliorées d’un ordre de grandeur par rapport aux TGBA. Utilisés dans l’approche hybride les TGTA se révèlent complémentaires aux TGBA.

10 years, 3 months

Vaucanson 2.0 is released!

by Akim Demaille

The Vaucanson Team is very happy to announce that Vancanson 2.0 was just released! It represents two years of development effort (and two days of documentation effort...). Vaucanson is a free-software platform for manipulating weighted rational expressions and automata (including transducers). It aims at genericity and efficiency (hence provides a fast low-level C++ API), but also at user friendliness (hence provides a high-level C++ API, a Python binding, and an IPython-powered interactive and visual shell). It is a joint project between Jacques Sakarovitch (Télécom Paritech), Sylvain Lombardy (LaBRI), Akim Demaille and Alexandre Duret-Lutz (LRDE/EPITA). Everything about this release is available here: https://vaucanson.lrde.epita.fr/Vaucanson2.0 A (partial) list of the user visible changes is available here: https://vaucanson.lrde.epita.fr/News_File A (way too short but regularly updated) documentation of the IPython interface can be found here: https://www.lrde.epita.fr/dload/vaucanson/2.0/notebooks/ Enjoy! Akim, Alexandre, Alfred, Antoine, Canh, Jacques, Luca and Sylvain

10 years, 5 months

[CfPart] International Lisp Conference 2014, August 15-17, Montreal

by Didier Verna

ILC 2014 - International Lisp Conference "Lisp on the Move" August 15-17 2014, Université de Montréal, Montréal, Canada Sponsored by the Association of Lisp Users In cooperation with: ACM SIGPLAN http://ilc2014.iro.umontreal.ca/ Latest News: * Only 4 days left before the early registration deadline! * Registration is now open. See http://ilc2014.iro.umontreal.ca/registration.php * Invited speakers announced. Christian Queinnec, Ambrose Bonnaire-Sergeant, Stefan Monnier, Marc Battyani. Scope: Lisp is one of the greatest ideas from computer science and a major influence for almost all programming languages and for all sufficiently complex software applications. The International Lisp Conference is a forum for the discussion of Lisp and, in particular, the design, implementation and application of any of the Lisp dialects. We encourage everyone interested in Lisp to participate. This year's focus is directed towards integrated solutions, including mobile computing. The conference also provides slots for lightning talks, to be registered on-site every day. The full programme is available here: http://ilc2014.iro.umontreal.ca/program.php Important Dates: - July 14, 2014: Early registration deadline - August 15, 2014: Conference starts Organizing Committee: General Chair: Marc Feeley (Université de Montréal, Montréal, Canada) Programme Chair: Didier Verna (EPITA Research lab, Paris, France) Local chair: Marc Feeley (Université de Montréal, Montréal, Canada) Programme Committee: Charlotte Herzeel, IMEC, ExaScience Life Lab, Belgium Dave Herman, Mozilla Research, USA Greg Pfeil, Clozure Associates, USA Irène Anne Durand, LaBRI University of Bordeaux, France Jim Newton, Cadence Design Systems, France Kuroda Hisao, Mathematical Systems Inc., Japan Matthew Might, University of Utah, USA Nicolas Neuss, Friedrich Alexander Universitat, Germany Ralf Möller, TUHH, Germany Sam Tobin-Hochstadt, Northeastern University, USA William Byrd, University of Utah, USA Contact: ilc14-organizing-committee at alu.org For more information, see http://ilc2014.iro.umontreal.ca/ -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

10 years, 5 months

← Newer
1
...
22
23
24
25
26
27
28
...
57
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