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
I am pleased to announce that I will hold a 90' session at the next
ACCU conference in Bristol, next April. The abstract is given below.
A Taste of Julia
Julia is a recent programming language developed at MIT and sold as a
high level, high performance dynamic language for scientific
computing. One of the co-authors of Julia has a Scheme background, and
in fact, it appears that Julia borrows a lot from Scheme, Common Lisp
and Dylan. This is to the point that Julia may even be considered as a
new Lisp dialect. This is enough, already, to catch our attention, but
there's more. Julia also seems to benefit from modern optimization
techniques for dynamic languages, notably through its LLVM based JIT
compiler. In this talk, we will give a tour of the language's most
prominent features, with a slight focus on what makes it a Lisp,
sometimes (not always) an even better one that the existing
alternatives.
--
Resistance is futile. You will be jazzimilated.
Lisp, Jazz, Aïkido: http://www.didierverna.info
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:
- *** Submission deadline extended to Saturday Feb 27 ***
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. The conference proceedings will be
published in the ACM Digital Library.
Important dates:
- *** EXTENDED *** 27 Feb 2016 Submission deadline *** EXTENDED ***
- 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, 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
Henry Lieberman — MIT, USA
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 very happy to announce the release of Vcsn 2.2! This version,
code-named "the lazy release", concludes the work from Antoine and Valentin,
who left EPITA for their final internship.
In addition to the usual load of improvements (more doc and less bugs), this
version features some noteworthy changes:
- several algorithms now offer a lazy variant: compose, conjunction,
derived_term, determinize, insplit, and proper. Instead of completing the
construction on invocation, the result is built incrementally, on demand,
e.g., when requested by an evaluation.
This is especially useful for large computations a fraction of which is
actually needed (e.g., composition of two large automata and then with a
small one), or for computations that would not terminate (e.g.,
determinization of some weighted automata).
- the functions `automaton.lightest` and `automaton.lightest_automaton`
explore the computations (i.e., paths of accepted words) with the smallest
weights (dubbed "shortest paths" for tropical-min semirings). They
feature several implementations controlled via the `algo` argument.
- rational expressions now support UTF-8 operators in input and output.
They also learned a few tricks to be better looking (e.g., `aaa` => `a³`).
- several new algorithms or improvements or generalizations of existing ones.
- a number of performance improvements.
More details are available on Vcsn’s web site.
People who worked on this release:
- Akim Demaille
- Antoine Pietri
- Lucien Boillod
- Nicolas Barray
- Raoul Billion
- Sébastien Piat
- Thibaud Michaud
- Valentin Tolmer
People who have influenced this release:
- Alexandre Duret-Lutz
- Jacques Sakarovitch
- Luca Saiu
Vcsn 2.2: http://vcsn.lrde.epita.fr/Vcsn2.2
Everything about Vcsn: http://vcsn.lrde.epita.fr
Online Vcsn: http://vcsn-sandbox.lrde.epita.fr
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 février 2016 (11h--12h), 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-02-17
[4] http://www.lrde.epita.fr/Contact
Au programme du Mercredi 17 février 2016 :
* 11h: Computing with (nearly) unlimited resources
-- Stephan Hadinger, Head of Solutions Architecture, AWS
https://aws.amazon.com
Le cloud computing donne accès à des ressources de stockage et de calcul
quasiment illimitées, pour un coût toujours plus bas. Devant l’explosion
de la quantité des données générées et le besoin de réagir toujours plus
vite, il n’a jamais été aussi facile d’accéder aux technologies de
traitement massif.
Nous illustrerons de nombreux cas d’usage du cloud : Hadoop,
dataware-house de plusieurs Po, traitement temps réel de millions
d’événements par seconde, IOT, Machine Learning…
En particulier, l’utilisation d’algorithmes massivement parallèles prend
toute son importance et permet de tirer pleinement parti de l’élasticité
du cloud, par exemple: Monte-Carlo dans le domaine financier,
modélisation de protéines en 3D pour du screening, analyse génomique,
analyse de logs…
-- Stephan Hadinger a fait une longue carrière dans l'IT, spécialisé dans
les domaines Infrastructure, B2C et B2B afin de permettre aux
entreprises de tirer un maximum de bénéfices de leurs investissements
technologiques. Dans son rôle d'Architecte Solutions avec Amazon Web
Services, Stephan travaille avec des entreprises françaises de toutes
tailles pour les aider à migrer vers le Cloud et utiliser leur IT pour
mieux servir leurs clients.
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