Merci de me désabonner de la liste
Cordialement
pierre(a)levillain.org
Le 10 mai 2016 à 12:00, <annonce-request(a)lrde.epita.fr> a écrit :
> Envoyez vos messages pour la liste Annonce à
> annonce(a)lrde.epita.fr
>
> Pour vous (dés)abonner par le web, consultez
> https://lists.lrde.epita.fr/listinfo/annonce
>
> ou, par email, envoyez un message avec 'help' dans le corps ou dans le
> sujet à
> annonce-request(a)lrde.epita.fr
>
> Vous pouvez contacter l'administrateur de la liste à l'adresse
> annonce-owner(a)lrde.epita.fr
>
> Si vous répondez, n'oubliez pas de changer l'objet du message afin
> qu'il soit plus spécifique que "Re: Contenu du digest de Annonce..."
>
>
> Thèmes du jour :
>
> 1. [Seminaire-LRDE] Mercredi 18 mai 2016: Didier Verna --
> EPITA/LRDE (Daniela Becker)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 10 May 2016 10:58:47 +0200
> From: Daniela Becker <daniela(a)lrde.epita.fr>
> To: seminaire(a)lrde.epita.fr
> Subject: [Lrde Annonce] [Seminaire-LRDE] Mercredi 18 mai 2016: Didier
> Verna -- EPITA/LRDE
> Message-ID: <F6E5FB42-E245-48DB-B367-D0FED0398B36(a)lrde.epita.fr>
> Content-Type: text/plain; charset="utf-8"
>
> 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 18 mai 2016 (11h--12h30), Salle L0 du LRDE.
>
> Vous trouverez sur le site du séminaire [1] les prochaines séances,
> les résumés, captations vidéos et planches des exposés précédents [2],
> le détail de cette séance [3] ainsi que le plan d'accès [4].
>
> [1] http://seminaire.lrde.epita.fr
> [2] http://seminaire.lrde.epita.fr/Archives
> [3] http://seminaire.lrde.epita.fr/2016-05-18
> [4] http://www.lrde.epita.fr/Contact
>
> Au programme du Mercredi 18 mai 2016 :
>
> * 11h: Un avant-goût de Julia
> -- Didier Verna -- EPITA/LRDE
> http://www.didierverna.info/
>
> Julia est un langage de programmation relativement jeune, développé au
> MIT, et vendu comme langage dynamique à haute performance pour le calcul
> scientifique numérique. L'un des co-auteurs du langage a une
> connaissance de Scheme, et Julia s'inspire en effet largement de Scheme,
> Common Lisp et Dylan, au point qu'il pourrait presque revendiquer un
> lien de parenté avec Lisp. Tout ceci est déjà suffisant pour capter
> notre attention, mais il y a plus: Julia semble également tirer parti de
> techniques modernes d'optimisation pour les langages dynamiques, en
> particulier grâce à son compilateur « Just-in-Time » basé sur LLVM.
>
> Dans cette présentation, nous ferons un tour des aspects les plus
> saillants du langage, avec une légère emphase sur ce qui en fait (ou
> pas) un Lisp, quelques fois même (pas toujours) un meilleur Lisp que
> Lisp lui-même.
>
> -- Didier Verna est enseignant-chercheur au Laboratoire de Recherche et
> Développement de l'EPITA. Il s'intéresse aux langages dynamiques
> multi-paradigmes et en particulier aux implications de l'homoiconicité
> (à tout le moins de la réflexivité) en termes de méta-programmation,
> d'extensibilité et de génie logiciel en général. Didier Verna préside le
> comité de pilotage du Symposium Européen sur Lisp. Il est également très
> impliqué dans le logiciel libre; il fût l'un des mainteneurs d'XEmacs
> pendant plus de 15 ans.
>
>
> 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
>
> ------------------------------
>
> Subject: Pied de page des remises groupées
>
> _______________________________________________
> Annonce mailing list
> Annonce(a)lrde.epita.fr
> https://lists.lrde.epita.fr/listinfo/annonce
>
>
> ------------------------------
>
> Fin de Lot Annonce, Vol 123, Parution 1
> ***************************************
>
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 18 mai 2016 (11h--12h30), Salle L0 du LRDE.
Vous trouverez sur le site du séminaire [1] les prochaines séances,
les résumés, captations vidéos et planches des exposés précédents [2],
le détail de cette séance [3] ainsi que le plan d'accès [4].
[1] http://seminaire.lrde.epita.fr
[2] http://seminaire.lrde.epita.fr/Archives
[3] http://seminaire.lrde.epita.fr/2016-05-18
[4] http://www.lrde.epita.fr/Contact
Au programme du Mercredi 18 mai 2016 :
* 11h: Un avant-goût de Julia
-- Didier Verna -- EPITA/LRDE
http://www.didierverna.info/
Julia est un langage de programmation relativement jeune, développé au
MIT, et vendu comme langage dynamique à haute performance pour le calcul
scientifique numérique. L'un des co-auteurs du langage a une
connaissance de Scheme, et Julia s'inspire en effet largement de Scheme,
Common Lisp et Dylan, au point qu'il pourrait presque revendiquer un
lien de parenté avec Lisp. Tout ceci est déjà suffisant pour capter
notre attention, mais il y a plus: Julia semble également tirer parti de
techniques modernes d'optimisation pour les langages dynamiques, en
particulier grâce à son compilateur « Just-in-Time » basé sur LLVM.
Dans cette présentation, nous ferons un tour des aspects les plus
saillants du langage, avec une légère emphase sur ce qui en fait (ou
pas) un Lisp, quelques fois même (pas toujours) un meilleur Lisp que
Lisp lui-même.
-- Didier Verna est enseignant-chercheur au Laboratoire de Recherche et
Développement de l'EPITA. Il s'intéresse aux langages dynamiques
multi-paradigmes et en particulier aux implications de l'homoiconicité
(à tout le moins de la réflexivité) en termes de méta-programmation,
d'extensibilité et de génie logiciel en général. Didier Verna préside le
comité de pilotage du Symposium Européen sur Lisp. Il est également très
impliqué dans le logiciel libre; il fût l'un des mainteneurs d'XEmacs
pendant plus de 15 ans.
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
We are happy to announce that the following paper was accepted to the
21st International Conference on Implementation and Application of
Automata (CIAA 2016).
Multitape Rational Expressions
Akim Demaille
EPITA/LRDE
We introduce (weighted) rational expressions to denote series over
Cartesian products of monoids. To this end, we propose the operator |
to build multitape expressions such as (a⁺|x + b⁺|y)*. We define
expansions, which generalize the concept of derivative of a rational
expression, but relieved from the need of a free monoid. We propose
an algorithm based on expansions to build multitape automata from
multitape expressions.
We are pleased to announce that the following paper has been accepted
for publication in the IEEE Transactions on Pattern Analysis and
Machine Intelligence (TPAMI). Find the title and abstract below.
Title and corresponding authors:
Hierarchical Segmentation Using Tree-Based Shape Spaces
Yongchao Xu(13), Edwin Carlinet(1), Thierry Geraud(1), Laurent Najman(2)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) LIGM, Équipe A3SI, ESIEE Paris, 93160 Noisy-le-Grand, France
(3) LTCI, CNRS, Téléecom ParisTech, 75013, Paris, France
Abstract:
Current trends in image segmentation are to compute a hierarchy of
image segmentations from fine to coarse. A classical approach to
obtain a single meaningful image partition from a given hierarchy is
to cut it in an optimal way, following the seminal approach of the
scale-set theory. While interesting in many cases, the resulting
segmentation, being a non-horizontal cut, is limited by the structure
of the hierarchy. In this paper, we propose a novel approach that acts
by transforming an input hierarchy into a new saliency map. It relies
on the notion of shape space: a graph representation of a set of
regions extracted from the image. Each region is characterized with an
attribute describing it. We weigh the boundaries of a subset of
meaningful regions (local minima) in the shape space by extinction
values based on the attribute. This extinction-based saliency map
represents a new hierarchy of segmentations highlighting regions
having some specific characteristics. Each threshold of this map
represents a segmentation which is generally different from any cut of
the original hierarchy. This new approach thus enlarges the set of
possible partition results that can be extracted from a given
hierarchy. Qualitative and quantitative illustrations demonstrate the
usefulness of the proposed method.
We are happy to announce the release of Spot 2.0!
Spot is a C++ library for model checking and manipulation
of temporal logic formula and omega-automata. It also
comes with command-line tools and Python bindings.
You can find the new release here:
http://www.lrde.epita.fr/dload/spot/spot-2.0.tar.gz
See https://spot.lrde.epita.fr/ for documentation and installation
instructions.
Spot 2.0 is the result of 28 months of work, as we starting working on
this branch after the release of Spot 1.2.1 (Dec 2013). It includes
contributions from Alexandre Lewkowicz, Amaury Fauchille, Étienne
Renault, Laurent Xu, Thibaud Michaud, and myself.
For people upgrading from Spot 1.2.6 (or older), the main news are as
follows:
* Automata now support acceptance conditions expressed as arbitrary
formulas over "marks" that must be seen infinitely often or
finitely often.
* The C++ API has been seriously overhauled and now requires a C++11
compiler. Backward compatibility has been broken in many ways:
see https://spot.lrde.epita.fr/upgrade2.html for help about
migrating old code. But now that the dust has settled, you should
not expect further API breakage in upcoming 2.x releases.
* The shell commands now include tools for processing automata. See
https://spot.lrde.epita.fr/tools.html for a list of all the tools,
and check https://spot.lrde.epita.fr/autfilt.html in particular.
The default interchange format is the Hanoi Omega
Automata format (HOA), but other formats are supported as well.
* The Python bindings are more complete, and even allow prototyping
low-level algorithms (for instance the page
https://spot.lrde.epita.fr/ipynb/product.html shows how to
implement a product of two automata with arbitrary acceptance).
Python bindings also interface nicely with IPython/Jupyter
notebooks. See https://spot.lrde.epita.fr/tut.html for short
examples of various tasks implemented in shell, C++, and Python.
For those upgrading from 1.99.9, the difference with Spot 2.0 is
rather thin. The following changes were included in Spot 2.0
(2016-04-11):
Command-line tools:
* ltlfilt now also support the --accept-word=WORD and
--reject-word=WORD options that were introduced in autfilt in the
previous version.
Python:
* The output of spot.atomic_prop_collect() is printable and
can now be passed directly to spot.ltsmin.model.kripke().
Library:
* digraph::valid_trans() renamed to digraph::is_valid_edge().
Documentation:
* The concepts page (https://spot.lrde.epita.fr/concepts.html) now
includes a highlevel description of the architecture, and some
notes aboute automata properties.
* More Doxygen documentation for spot::formula and spot::digraph.
See https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0/NEWS for the
complete history of NEWS entries across previous releases.
Please direct any feedback to <spot(a)lrde.epita.fr>.
--
Alexandre Duret-Lutz
ELS'16 - 9th European Lisp Symposium
Department of Computer Science
AGH University of Science and Technology
Kraków, Poland
May 9-10, 2016
In cooperation with: ACM SIGPLAN
Sponsored by EPITA, Franz Inc., LispWorks Ltd., IdEx
and Dept. of Computer Science AGH UST
http://www.european-lisp-symposium.org/
Recent news:
- Full programme now available online
- Registration now open (early registration deadline: April 25)
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.
Keynote speakers:
- Pierre Castéran -- Program Proving with Coq
- Stephan Karpinski -- Julia: to Lisp or Not to Lisp?
- Francis Sergeraert -- Lexical Closures and Complexity
Important dates:
- 25 Apr 2016 Early registration deadline
- 9-10 May 2016 Symposium
Programme chair:
Irène Durand, LaBRI, University of Bordeaux, France
Local chair:
Michał Psota, Emergent Network Defense, Kraków, Poland
Programme committee:
Antonio Leitao — INESC-ID / Instituto Superior Técnico, Universidade
de Lisboa, Portugal
Charlotte Heerzel — IMEC, Leuven, Belgium
Christian Queinnec — University Pierre et Marie Curie, Paris 6, France
Christophe Rhodes — Goldsmiths, University of London, United Kingdom
Didier Verna — EPITA Research and Development Laboratory, France
Erick Gallesio — University of Nice-Sophia Antipolis, France
François-René Rideau, Google, USA
Giuseppe Attardi — University of Pisa, Italy
Kent Pitman, HyperMeta Inc., USA
Leonie Dreschler-Fischer — University of Hamburg, Germany
Pascal Costanza — Intel Corporation, Belgium
Robert Strandh — University of Bordeaux, France
Search Keywords:
#els2016, ELS 2016, ELS '16, European Lisp Symposium 2016,
European Lisp Symposium '16, 9th ELS, 9th European Lisp Symposium,
European Lisp Conference 2016, European Lisp Conference '16
--
Resistance is futile. You will be jazzimilated.
Lisp, Jazz, Aïkido: http://www.didierverna.info
We are pleased to announce that the following paper has been accepted
for publication in the International Journal on Software Tools for Technology
Transfer (STTT). Find the title and abstract below.
Title and corresponding authors:
Variations on Parallel Explicit Emptiness Checks for Generalized Büchi Automata
Etienne Renault(1), Alexandre Duret-Lutz(1), Fabrice Kordon(2,3) and Denis Poitrenaud(3,4)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) Sorbonne Universités, UPMC Univ. Paris 06, France
(3) CNRS UMR 7606, LIP6, F-75005 Paris, France
(4) USPC, Université Paris Descartes, Paris, France
Abstract:
We present new parallel explicit emptiness checks for LTL model
checking. Unlike existing parallel emptiness checks, these are
based on a Strongly Connected Component (SCC) enumeration,
support generalized Büchi acceptance, and require no synchronization
points nor recomputing procedures. A
salient feature of our algorithms is the use of a global union-find
data structure in which multiple threads share structural
information about the automaton checked.
Besides these basic algorithms, we present one architectural variant
isolating threads that write to the union-find, and one extension
that decomposes the automaton based on the strength of its
SCCs to use more optimized emptiness checks.
The results from an extensive experimentation of our algorithms and
their variations show encouraging performances, especially when the
decomposition technique is used.
We are happy to announce that our paper entitled
Type-Checking of Heterogeneous Sequences in Common Lisp
authored by Jim Newton, Akim Demaille, and Didier Verna has been
accepted for presentation and publication at the
9th European Lisp Symposium (http://www.european-lisp-symposium.org).
Abstract:
We introduce the abstract concept of rational type expression and show its
relationship to rational language theory. We further present a concrete
syntax, regular type expression, and a Common Lisp implementation
thereof which allows the programmer to declaratively express the types of
heterogeneous sequences in a way which is natural in the Common Lisp
language. The implementation uses techniques well known and well founded
in rational language theory, in particular the use of the Brzozowski derivative
and deterministic automata to arrive at a solution which can match a
sequence in linear time. We illustrate the concept with several motivating
examples, and finally explain many details of its implementation.
Please find the link to the article and a longer more elaborate project report
here: https://www.lrde.epita.fr/wiki/Publications/newton.16.els.inc
If you have any questions or comments about the paper, we are happy
to discuss them with you.
Jim
Bonjour à tous,
La prochaine séance du séminaire MeFoSyLoMa sera orientée outils, et
se tiendra au LRDE.
========================================================================
Séminaire MeFoSyLoMa
http://www.mefosyloma.fr/
Méthodes Formelles pour Les Systèmes Logiciels et Matériels
Vendredi 8 avril 2016, 14h-17h
Adresse:
LRDE (Epita), Salle Alpha
Bâtiment X, 2e étage
18 rue Pasteur, 94270 Le Kremlin-Bicêtre
Métro Porte d'Italie
Plans d'accès :
https://www.google.com/maps?q=48.8152808,2.3623765https://www.lrde.epita.fr/~adl/dl/acces-lrde.pdf
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: Alexandre Duret-Lutz (LRDE/Epita)
Spot 2.0
Je présenterai Spot 2.0, une bibliothèque C++ de manipulation
d'omega-automates pour le model checking. Les nouveautés sont assez
nombreuses: la bibliothèque travaille maintenant avec des automates
dont la condition d'acceptation peut être arbitrairement complexe (par
exemple une combinaison booléenne de Streett et Rabin généralisé), de
nouveaux outils en ligne de commande permettent de manipuler et
produire ces automates, et la majeur partie des fonctionnalités est
utilisable avec une surcouche de bindings pour Python.
Je montrerai en particulier:
- des exemples d'utilisation tirés du cours d'initiation au model
checking de l'Epita (travail sur la sémantique de LTL, et écriture
d'un model checker jouet en quelques lignes de Python).
- la facilité avec laquelle on peut chaîner les différents outils
pour construire un pipeline de manipulation d'automates
- une technique utilisant un SAT-solver pour synthétiser des
automates équivalents mais avec d'autres conditions d'acceptation.
14h45-15h30: Maximilien Colange (ENS de Cachan)
Je présenterai TiAMo, un model-checker pour les systèmes temporisés
développé au LSV. Les systèmes temporisés présentent une composante en
temps continu, qui font de leurs espaces d'états des graphes infinis à
branchement infini. Dans le cadre du model-checking, leur analyse
repose essentiellement sur des abstractions permettant de se ramener à
des graphes discrets. Nous nous concentrons sur les problèmes
d'accessibilité dans les automates temporisés, et d'accessibilité
optimale dans les automates temporisés à coûts positifs.
TiAMo est pensé comme une plateforme permettant la comparaison
expérimentale des différents algorithmes et abstractions pour la
vérification de systèmes temporisés. Je rappellerai les principaux
problèmes algorithmiques qui se posent dans ce cadre, et les
différentes solutions qui ont été proposées. Je présenterai également
l'outil TiAMo, et les algorithmes d'analyse qu'il implémente.
15h30-16h00: pause café
16h00: vie du groupe
========================================================================
--
Alexandre Duret-Lutz