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 14 juin 2017 (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/2017-06-14
[4] http://www.lrde.epita.fr/wiki/Contact
Au programme du Mercredi 14 juin 2017 :
* 11h--12h: MAQAO: une suite d'outils pour l'analyse et l’optimisation
des performances
-- Andrés S. Charif Rubial (ESN PeXL et Li-PARAD - Université de
Versailles)
www.maqao.org
MAQAO (Modular Assembly Quality Analyzer and Optimizer) est une
suite
d'outils d'analyse et d'optimisation des performances à destination
d'applications binaires. Le but principal de MAQAO est d'analyser des
codes binaires puis de proposer aux développeurs d'applications des
rapports synthétiques les aidant à comprendre et optimiser les
performances de leur application. MAQAO combine des analyses
statiques
(évaluation de la qualité du code) et dynamiques (profiling) basées
sur
la capacité à reconstruire des structures aussi bien bas niveau
(basic
blocks, instructions, etc.) que haut niveau (fonctions et boucles).
Un
autre aspect important de MAQAO est son extensibilité. En effet les
utilisateurs peuvent écrire leur propre plugin grâce à un langage de
script simple intégré (Lua).
-- Le Dr. Andres S. CHARIF RUBIAL dirige aujourd'hui une ESN dont les
principales activités sont le HPC, l’ingénierie système, réseau et
sécurité. En parallèle il est chercheur hébergé au Laboratoire
Li-PARAD
de l'Université de Versailles. Il a dirigé pendant 4 ans l'équipe de
recherche et développement "évaluation des performance" du
laboratoire
Exascale Computing Research Laboratory (situé sur le campus Teratec).
Il
a principalement supervisé et travaillé au développement de la suite
d'outils MAQAO afin de mieux comprendre les problèmes de performance
des
applications HPC mono et multi-noeuds. Ses travaux de thèse achevés
en
2012 portaient d'ailleurs déjà sur cette thématique, en particulier
sur
le profilage d'applications et les problématiques de caractérisation
des
performances mémoire sur des systèmes à mémoire partagée.
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.
--
Guillaume TOCHON
Maître de conférences // Assistant Professor
LRDE, EPITA
18, rue Pasteur
94270 Le Kremlin-Bicêtre
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/seminaire
> Début du message réexpédié :
>
> The peer review process for Interspeech 2017 is now completed. Each and every paper has received at least 3 reviews, and the Technical Program Committee has thoroughly analyzed the scores and comments of the reviewers to put together an exciting technical program for the conference. Given the large number of high-quality submissions received, this has proved to be a difficult task, and many interesting papers could not be included. This year the overall acceptance rate is about 50%.
>
> We are pleased to inform you that your paper:
>
> Paper ID: 537
> Title: The MIT-LL, JHU and LRDE NIST 2016 Speaker Recognition
> Evaluation System
>
> has been selected for a presentation at the conference.
I'm happy to announce that the following article has been accepted for
publication in the International SPIN Symposium on Model Checking of
Software (SPIN'17), to be held in Santa Barbara on July 13-14, 2017.
« Explicit State Model Checking with
Generalized Büchi and Rabin Automata »
Vincent Bloemen¹ Alexandre Duret-Lutz² Jaco van de Pol¹
¹ University of Twente, Enschede, The Netherlands
² LRDE / EPITA, Le Kremlin-Bicêtre, France
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 transition-based generalized Rabin automata
(TGRAs), improves the model checking procedure. TGRAs can have
significantly fewer states than TGBAs, however 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. We observed that our algorithm can be used to
replace a TGBA checking algorithm without losing performance. In
general, we found little to no improvement by checking TGRAs directly.
http://www.lrde.epita.fr/dload/papers/bloemen.17.spin.pdf
--
Alexandre Duret-Lutz