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 4 juillet 2012 (14h00-17h00).
Au programme:
* 14h: Vérification efficace de propriétés insensibles au bégaiement.
-- Ala Eddine Ben Salem (doctorant)
Le model checking est une technique de vérification formelle
automatique. Prenant en entrée un modèle décrivant toutes les exécutions
possibles du système et une propriété exprimée sous la forme d'une
formule de logique temporelle, un algorithme de model checking répond si
le modèle satisfait ou non la formule. Le problème principal du
model-checking est l'explosion combinatoire de l'espace d'états
décrivant le système.
Afin d'améliorer les performances, on a apporté les contributions
suivantes à l'approche automate du model checking. D'abord
l'amélioration de l'algorithme de vérification en deux passes de
l'approche basée sur les automates Testeur TA (Testing Automaton).
Ensuite la proposition d'une méthode permettant de transformer un
automate TA en un automate vérifiable en une seule passe, qu'on a appelé
STA (Single-pass Testing Automaton). Enfin, la contribution la plus
significative est un nouveau type d'automate baptisé TGTA
(Transition-based Generalized Testing Automaton). L'apport principal de
cette nouvelle approche consiste à proposer une méthode permettant de
supprimer les transitions bégayantes dans un TGTA sans avoir besoin, ni
d'ajouter une seconde passe comme dans l'approche TA, ni d'ajouter un
état artificiel comme dans l'approche STA.
-- A.E. Ben Salem est ingénieur ENSEEIHT-2005 en Informatique et
Mathématiques Appliquées, il a obtenu en parallèle un Master Recherche
Sûreté du Logiciel et Calcul à haute Performance à l’INP Toulouse.
Depuis 2011, il est doctorant au LRDE et au LIP6 sur la vérification
formelle de propriétés sur des systèmes logiciels, en lien avec le
projet Spot.
* 15h30: Composition dynamique de techniques pour le model checking efficace
-- Étienne Renault (doctorant)
Le model checking est une technique qui permet de s'assurer qu'un
système vérifie un ensemble de caratéristiques appelées propriétés. Le
système et la négation de la formule sont ensuite représentés de manière
abstraite (ici un automate) pour pouvoir détecter des comportements
incohérents. Ces propriétés ont été classifiées et possèdent des
particularités qui peuvent être exploitées afin de réduire la complexité
du processus de vérification. Nous montrerons ici comment tirer parti
dynamiquement des différentes classes de formules.
-- E. Renault est diplômé de Paris VI en système et applications
réparties, il s'intéresse à la vérification formelle des systèmes
concurents. Il a intégré cette année le LRDE dans le cadre de sa thèse
portant sur la composition dynamique de techniques pour le model
checking efficace. Ce travail, en collaboration avec l'équipe MoVe du
Lip6, s'intègre au projet Spot.
* 15h30: Filtrage morphologique dans les espaces de formes : Applications avec la représentation d'image par arbres
-- Yongchao Xu (doctorant)
(Morphological Filtering in Shape Spaces: Applications using Tree-Based
Image Representations)
Connected operators are filtering tools that act by merging elementary
regions of an image. A popular strategy is based on tree-based image
representations: for example, one can compute a shape-based attribute on
each node of the tree and keep only the nodes for which the attribute is
sufficiently strong. This operation can be seen as a thresholding of the
tree, seen as a graph whose nodes are weighted by the attribute. Rather
than being satisfied with a mere thresholding, we propose to expand on
this idea, and to apply connected filters on this latest graph.
Consequently, the filtering is done not in the image space, but in the
space of shapes built from the image. Such a processing is a
generalization of the existing tree-based connected operators. Indeed,
the framework includes classical existing connected operators by
attributes. It also allows us to propose a class of novel connected
operators from the leveling family, based on shape attributes. Finally,
we also propose a novel class of self-dual connected operators that we
call morphological shapings.
-- Yongchao Xu received the B.S. degree in optoelectronic engineering from
Huazhong University of Science and Technology, China, in 2008, the
"diplôme d'ingénieur" in electronic & embedded system at Polytech'
Paris-Sud and the M.S. degree in signal & image processing from
Université Paris Sud, in 2010. He is currently a PhD student at
Université Paris Est working on image segmentation, morphological image
analysis and, especially shape-based connected morphology.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
