I'm happy to announce that my contribution to TUG 2011, the next TeX
Users Group International conference, has been accepted. Please find the
title and abstract below.
LaTeX Coding Standards
Because LaTeX (and ultimately TeX) is only a macro-expansion system, the
language does not impose any kind of good software engineering practice,
program structure or coding style whatsoever. As a consequence, writing
beautiful code (for some definition of "beautiful") requires a lot of
self-discipline from the programmer.
Maybe because in the LaTeX world, collaboration is not so widespread
(most packages are single-authored), the idea of some LaTeX Coding
Standards is not so pressing as with other programming languages. Some
people may, and probably have developed their own programming habits,
but when it comes to the LaTeX world as a whole, the situation is close
to anarchy.
Over the years, the permanent flow of personal development experiences
contributed to shape my own taste in terms of coding style. The issues
involved are numerous and their spectrum is very large: they range from
simple code layout (formatting, indentation, naming schemes etc.),
mid-level concerns such as modularity and encapsulation, to very
high-level concerns like package interaction/conflict management and
even some rules for proper social behavior.
In this talk, I will report on all these experiences and describe what I
think are good (or at least better) programming practices. I believe
that such practices do help in terms of code readability,
maintainability and extensibility, all key factors in software
evolution. They help me, perhaps they will help you too.
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
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.
* 14h30: 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
Hello,
it is my pleasure to announce that I will hold a 2 hours tutorial on
Lisp extensibility and its impact on DSL implementation at the next
International Lisp Conference, Kyoto, Japan, October 2012.
For more information, please consult:
http://international-lisp-conference.org/2012/tutorials.html
--
Resistance is futile. You will be jazzimilated.
Scientific site: http://www.lrde.epita.fr/~didier
Music (Jazz) site: http://www.didierverna.com
EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France
Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22
