I am happy to announce that the following two papers have been
accepted at the 22nd International SPIN Symposium on Model Checking of
Software (SPIN 2015) to be held in Stellenbosch, South Africa on 24–26
August 2015.
---
On Refinement of Büchi Automata for Explicit Model Checking
František Blahoudek¹, Alexandre Duret-Lutz²,
Vojtěch Rujbr¹, and Jan Strejček¹
¹Faculty of Informatics, Masaryk University, Brno, Czech Republic
²LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/blahoudek.15.spin
Abstract:
In explicit model checking, systems are typically described in an
implicit and compact way. Some valid information about the system
can be easily derived directly from this description, for example
that some atomic propositions cannot be valid at the same time. The
paper shows several ways to apply this information to improve the
Büchi automaton built from an LTL specification. As a result, we get
smaller automata with shorter edge labels that are easier to
understand andmore importantly, for which the explicit model
checking process performs better.
---
Practical Stutter-Invariance Checks for ω-Regular Languages
Thibaud Michaud and Alexandre Duret-Lutz
LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/michaud.15.spin
Abstract:
We propose several automata-based constructions that check whether a
specification is stutter-invariant. These constructions assume that
a specification and its negation can be translated into Büchi
automata, but aside from that, they are independent of the
specification formalism. These transformations were inspired by a
construction due to Holzmann and Kupferman, but that we broke down
into two operations that can have different realizations, and that
can be combined in different ways. As it turns out, implementing
only one of these operations is needed to obtain a functional
stutter-invariant check. Finally we have implemented these
techniques in a tool so that users can easily check whether an LTL
or PSL formula is stutter-invariant.
--
Alexandre Duret-Lutz
About 10,000 hours (on the calendar, not of work!) after its first public
release, the Vcsn team is very happy to announce the release of Vcsn 2.1!
Vcsn is a platform for weighted automata and rational expressions.
It consists of an efficient C++ generic library, shell tools, Python
bindings, and a graphical interactive environment on top of IPython.
It is quite hard to cherry-pick a few new features that have been added in
Vcsn 2.1, as shown by the 4k+ lines in the NEWS file since 2.0. For
details, see http://vcsn.lrde.epita.fr/Vcsn2.1.
However, here are a few headlines:
- Many pages of documentation and examples have been written (see
http://vcsn.lrde.epita.fr/dload/2.1/notebooks).
- Now http://vcsn-sandbox.lrde.epita.fr/ provides a live demo.
- Packages for popular distributions (including for Docker) are already
available to simplify the installation.
- Transducers are much better supported, with improved syntax and several
algorithms (e.g., letterize, synchronize, partial_identity, is_functional,
etc.)
- Expressions now offer several sets of identities specifying how they
should be normalized. More generally, input/output of expressions have
been improved to match most users' expectations. New operators are
accepted: `&` for conjunction, `:` for shuffle, `&:` for infiltration,
`{c}` (postfix) for complement, and `<+` for deterministic choice.
- When entering an automaton (e.g., with `%%automaton` in IPython) user
state names are preserved.
- Of course, many bugs were fixed, many algorithms were sped up, and
internal details have been cleaned up.
- As Easter eggs, many features have also been added, but not advertised,
until we are sure of how we want them to look like.
People who worked on this release:
- Akim Demaille
- Antoine Pietri
- Canh Luu
- Clément Démoulins
- Lucien Boilod
- Nicolas Barray
- Sébastien Piat
- Sylvain Lombardy
- Valentin Tolmer
- Yann Bourgeois--Copigny
People who have influenced this release:
- Alexandre Duret-Lutz
- Jacques Sakarovitch
- Luca Saiu
To download Vcsn 2.1, and for any information, visit <http://vcsn.lrde.epita.fr/Vcsn2.1>.
Chers collègues,
j'ai le plaisir de vous annoncer qu'ELS, le Symosium Européen sur Lisp,
vient d'obtenir le statut de conférence « In Cooperation with: ACM
SIGPLAN ». Les actes seront donc désormais publiés dans leur Digital
Library.
--
My new Jazz CD entitled "Roots and Leaves" is out!
Check it out: http://didierverna.com/records/roots-and-leaves.php
Lisp, Jazz, Aïkido: http://www.didierverna.info
ELS'16 - 9th European Lisp Symposium
AGH University of Science and Technology
Kraków, Poland
May 9-10, 2016
http://www.european-lisp-symposium.org/
Sponsored by EPITA and AGH University
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 9th 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 classification categories and terms. For more
information on the submission guidelines and the ACM keywords, see:
http://www.acm.org/sigs/publications/proceedings-templates and
http://www.acm.org/about/class/1998.
Important dates:
- 19 Feb 2016 Submission deadline
- 25 Mar 2016 Notification of acceptance
- 15 Apr 2016 Early registration deadline
- 22 Apr 2016 Final papers due
- 9-10 May 2016 Symposium
Programme chair:
Irène Durand, 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
Francois-René Rideau, Google, USA
Giuseppe Attardi — University of Pisa, Italy
Henry Lieberman — MIT, USA
Kent Pitman, HyperMeta Inc., U.S.A.
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
--
My new Jazz CD entitled "Roots and Leaves" is out!
Check it out: http://didierverna.com/records/roots-and-leaves.php
Lisp, Jazz, Aïkido: http://www.didierverna.info
Chers collègues,
Pour la prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) il y a un changement
de date et d’horaire : elle aura lieu le Mercredi 14 octobre 2015 à 11h30--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/2015-10-14
[4] http://www.lrde.epita.fr/Contact
Au programme du Mercredi 14 octobre 2015 :
* 11h30: Intégrales de Morton pour la Simplification Géométrique Haute Vitesse
-- Tamy Boubekeur, Telecom ParisTech - CNRS - University Paris-Saclay
http://perso.telecom-paristech.fr/~boubek/
Le traitement géométrique 3D temps-réel a progressivement atteint un
niveau de performance rendant un grand nombre de primitives inspirées du
traitement du signal compatible avec les applications interactives. Cela
a souvent été rendu possible grâce à la co-conception des opérateurs,
des structures de données et du support matériel d’exécution. Parmi les
principales classes d'opérateurs géométriques, le filtrage et le
sur-échantillonnage (par raffinement) ont été exprimés sous des
contraintes temps-réel avec succès. Cependant, l'opérateur de
sous-échantillonnage --- la simplification adaptative --- demeure un cas
problématique pour les données non triviales.
Dans ce contexte, nous proposons un nouvel algorithme de simplification
géométrique rapide basé sur un nouveau concept : les intégrales de
Morton. En sommant les quadriques d'erreurs associées aux échantillons
géométriques selon leur ordre de Morton, notre approche permet
d'extraire de manière concurrente les nœuds correspondants à une coupe
adaptative dans la hiérarchie implicite ainsi définie, et d'optimiser la
position des sommets du maillage simplifié en parallèle. Cette méthode
est inspirée des images intégrales et exploite les avancées récentes en
construction et parcours haute performance de hiérarchies spatiales.
L'implémentation GPU de notre approche peut simplifier des maillages
composés de plusieurs millions d'éléments à un taux de rafraîchissement
interactif, tout en fournissant une géométrie simplifiée de qualité
supérieure aux méthodes uniformes et en préservant notamment les
structures géométriques saillantes. Notre algorithme est compatible avec
les maillages indexés, les soupes polygonales et les nuages de points,
et peut prendre en compte des attributs de surfaces (normal ou couleur
par exemple) et des métriques d'erreurs alternatives.
-- Tamy Boubekeur est Professeur en Science Informatique à Télécom
ParisTech (Institut Mines-Télécom, CNRS UMR 5141, Université
Paris-Saclay). Il mène ses activités de recherche dans le domaine de
l’informatique graphique 3D, s'intéressant tout particulièrement à la
modélisation et à la synthèse de formes, de matières et d’animation 3D
numériques, mais également aux systèmes visuels interactifs à hautes
performances.
-- De 2004 à 2007, il a été membre de l’INRIA Bordeaux (France) et
chercheur invité régulier à l’Université de Colombie Britannique à
Vancouver (Canada). Il a obtenu son Doctorat en Informatique à
l’Université des Sciences et Technologies de Bordeaux en 2007. Par la
suite, il a rejoint l’Unversité Technique de Berlin (TU Berlin) comme
chercheur associé. En 2008, il a rejoint le Département de Traitement du
Signal et des Images de Télécom ParisTech comme Maître de Conférences et
a créé le groupe d’informatique graphique. Il a obtenu son Habilitation
à Diriger des Recherches (HDR) en Informatique à l’Université Paris XI
en 2012 avant de devenir Professeur à Télécom ParisTech en 2013.
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.
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/seminaire