Vu sur epita.assos, je me suis dis que ca pouvait interesser des gens...
Bonjour a tous,
AéroIPSA, Le Centre National d'Etudes Spatiales et l'association Planète
Sciences Ile-de-France sont heureux de vous inviter au 3e Festiciel Espace
Ile-de-France qui se tiendra dimanche 11 juin 2006 de 11h à 18h au Parc
François Mitterrand de Saint-Pierre-du-Perray (91).
Au programme :
- animations astronomiques tous publics
- expositions sur le Soleil
- présentation d'une véritable capsule spatiale russe Photon
- mini-conférences
... et lancement de fusées à partir de 11heures.
Venez très nombreux (accès libre) !
Renseignements au 01 69 89 75 27
et sur www.saint-pierre-du-perray.fr
ou http://aeroipsa.forumactif.com/
Cyril ARNODO
Président d'AéroIPSA
--
SIGOURE Benoit aka Tsuna
_____
/EPITA\ Promo 2008.CSI Rock & tRoll
Bonjour,
Vous êtes cordialement invités à assister au séminaire qui aura lieu le
mercredi 14 juin à 14 heures en amphi P04 (KB).
-----------------------------------------------------------------------
Le programme :
*OLENA & TRANSFORMERS*
http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-06-14
OLENA
14h00 : Dynamisation de bibliothèques C++ statiques -- Tristan Croiset
14h30 : Conception d'un langage statique, un aperçu de SCOOL -- Q.
Hocquet T. Moulard
TRANSFORMERS
15h45 : Aperçu des Grammaires Attribuées -- Nicolas Pierron
16h15 : eXtended Reactive Modules -- Benoît Sigoure
-----------------------------------------------------------------------
Les Résumés des exposés :
*************************
OLENA
* Dynamisation de bibliothèques C++ statiques -- Tristan Croiset
L'utilisation de bibliothèques statiques en C++ est fréquente notamment
pour proposer des ensembles d'outils de traitements scientifiques. Cette
approche qui permet un développement plus efficace et une importante
généricité, cause plusieurs désavantages à l'utilisation et
particulièrement des temps de compilation rédhibitoires.
Nous avons donc cherché à proposer un pont qui permette de faciliter
l'utilisation de ces bibliothèques dans un contexte purement dynamique.
Plusieurs travaux ont déjà été réalisés au sein du laboratoire et ont
permis d'une part d'en préciser les besoins et d'autre part de démontrer
sa faisabilité. Les solutions retenues conservent l'utilisation du C++
et font appel aux bibliothèques statiques via une compilation « juste à
temps ».
Ce séminaire sera axé sur la proposition d'une solution simple qui doit
allier un fonctionnement parfaitement décrit et délimité avec une
souplesse suffisante. Nous verrons ensuite comment ce socle stable
pourra ensuite servir de base à des extensions d'usage (« sucres ») pour
différents cas d'utilisations.
* Conception d'un langage statique, un aperçu de SCOOL -- Q. Hocquet T.
Moulard
Lors du développement d'Olena, deux bibliothèques ont été créées afin de
contourner les différentes limitations du C++ : Metalic et Static.
Cependant, l'utilisation de ces dernières est loin d'être simple pour un
développeur qui ne connaît pas les mécanismes de fonctionnement interne
de ces outils. L'utilisation abondante de templates et des subtilités
associées à ces derniers rend, de plus, la compréhension de ces
bibliothèques difficile.
Afin de permettre une écriture simple, la création d'un langage
suffisamment expressif pour incorporer dans sa syntaxe les
fonctionnalités de Metalic et Static a été décidé. Ce langage doit
également être très performant afin de satisfaire les contraintes de
rapidité d'exécution liées à Olena. C'est de ce constat qu'est né SCOOL,
un langage statique orienté objet.
SCOOL est un langage transformé vers C++ : le « compilateur » génère des
fichiers C++ qui sont ensuite compilés classiquement. Dans cette
optique, il est possible d'incorporer du code C++ directement dans
SCOOL. Cette transformation n'est malheureusement pas aisée, à cause de
la grande complexité de Metalic, Static ainsi que de la grammaire du C++.
Ce séminaire se déroulera en deux parties. Tout d'abord un aperçu des
fonctionnalités de SCOOP et de sa syntaxe seront expliqués, puis nous
passerons à la façon de transformer cette syntaxe en C++.
TRANSFORMERS
* Aperçu des Grammaires Attribuées -- Nicolas Pierron
La notion de grammaire attribuée fut introduite par Knuth en 1968. Cette
notion permet l'implémentation de certaines passes des compilateurs actuels.
Les attributs sont des symboles attachés aux règles de la grammaire, ils
portent une information telle que le résultat d'une évaluation ou bien
une table de symboles. L'information peut être propagée entre les
attributs en suivant les règles de la grammaire. Plusieurs types de
propagations d'attributs existent, des propagations de haut en bas, de
bas en haut, et de gauche à droite. Ces catégories se répartissent sous
les noms de L-attributs, S-attributs, et LR-attributs.
Les grammaires attribuées permettent de faire de la désambiguïsation, ou
de la vérification de types, ... De même, il existe quelques systèmes
qui gèrent certains types de propagations, en vérifiant les problèmes de
cycles à la compilation de l'évaluateur tel que UU-AG, et le module
sdf-attribute du projet Transformers.
Cet exposé vous donnera un aperçu des grammaires attribuées, ainsi que
des propagations possibles et de la sémantique associée.
* eXtended Reactive Modules -- Benoît Sigoure
Reactive Modules est un formalisme utilisé pour modéliser des systèmes
concurrents. De nombreuses applications de model-checking se basent
dessus, dont PRISM. Ce dernier utilise un langage du même nom basé sur
une version simplifiée de Reactive Modules.
Le langage PRISM a été adopté comme un standard de facto et est utilisé
(entre autres) par APMC. Il a néanmoins plusieurs faiblesses : les seuls
types disponibles sont les entiers et les booléens, il n'existe pas de
structures de contrôle (if, for, etc..).
Ce dernier point est probablement le plus gênant car lorsqu'il s'agit de
décrire des systèmes conséquents, la spécification devient vite pénible.
Certaines personnes mettent au point des solutions « ad hoc » pour
pallier ce problème : l'utilisation de scripts shell, du préprocesseur
du C (cpp) ou du langage M4 sont des exemples courants. C'est pourquoi
eXtended Reactive Modules (XRM) à été créé. Ce package fournis des
outils qui permettent de travailler avec une version étendue du langage
PRISM. Néanmoins, comme il faut rester compatible avec le parseur de
PRISM de base, il faut traduire les systèmes écrits dans la version
étendue du langage vers du code PRISM pur.
Durant la présentation, nous verrons quelles sont les extensions et les
outils proposés par XRM, ainsi que leur fonctionnement, dans le but de
faciliter la description de systèmes en PRISM.
--
Daniela Becker
Responsable administrative du LRDE
--
Daniela Becker
Responsable administrative du LRDE
Bonjour,
Vous êtes tous cordialement invités à assister au séminaire qui aura
lieu le mercredi 7 juin à 14 heures en amphi P01 (KB).
-----------------------------------------------------------------------
Le programme :
*BDD, ALGORITHMES GENETIQUES & MARKOV*
http://www.lrde.epita.fr/cgi-bin/twiki/view/Publications/Seminar-2006-06-07
BDD
14h00 : BDD distribués et Java -- Guillaume Guirado
14h30 : Répartition des DDD en Erlang -- Samuel Charron
ALGORITHMES GENETIQUES
15h00 : Programmation génétique & Corewar -- Jérémy Marc
MARKOV
15h45 : Vérification du locuteur -- Charles-Alban Deledalle
16h15 : Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester
16h45 : Chaînes de Markov continues en présence d'incertitudes --
Nicolas Neri
-----------------------------------------------------------------------
Les Résumés des exposés :
*************************
BDD
* BDD distribués et Java -- Guillaume Guirado
Les BDD (Diagrammes de Décision Binaires) ont été très largement étudiés
depuis leur introduction à la fin des années 80. De très nombreuses
implémentations ont d'ailleurs été proposées.
Cependant, rares sont les bibliothèques permettant de distribuer notre
diagramme sur un cluster. Partant de ce constat, l'implémentation, dans
un langage moderne, d'une bibliothèque de gestion de BDD permettant la
répartition sur un grand nombre de machines est nécessaire. Cela
permettra d'augmenter considérablement la mémoire disponible, et donc de
résoudre des problèmes plus complexes. Pour cela, nous avons choisi le
langage Java.
Durant la présentation, nous verrons les principales propriétés des BDD
et leurs opérations. Ensuite, nous analyserons les résultats d'une
implémentation non répartie, avant de finalement exposer les choix,
forces et faiblesses, de notre bibliothèque répartie.
* Répartition des DDD en Erlang -- Samuel Charron
Les DDD (Data Decision Diagrams) généralisent le concept de BDD, en
permettant de ne pas se limiter aux fonctions booléennes. Cependant, ils
n'apportent pas de solution supplémentaire au problème de mémoire.
La répartition de BDD a déjà été longuement étudiée sans donner de
résultat réellement satisfaisant. Une étude sur les propriétés des DDD
nous a permis de réaliser la répartition. Nous utilisons pour cela
Erlang, un langage intégrant des primitives de communications et de
parallélisation
Lors de ce séminaire, nous vous présenterons les DDD. Ensuite, une
introduction à Erlang et a l'implémentation réalisée sera effectuée.
Enfin, nous comparerons plusieurs algorithmes de répartition existants
sur les BDD en y ajoutant d'autres algorithmes nouveaux.
ALGORITHMES GENETIQUES
* Programmation génétique & Corewar -- Jérémy Marc
Les algorithmes génétiques existent depuis les années 80 et constituent
une catégorie à part dans l'algorithmique évolutionnaire. Directement
inspirés de la nature, ou plus exactement de la biologie, ils ont pour
but d'approcher les solutions optimales en faisant varier les paramètres
caractéristiques des individus.
Lorsque ces individus sont des programmes, qui plus est en assembleur de
type Corewar, la tâche devient nettement plus ardue. En effet il devient
complexe d'exhiber ces paramètres et difficile de les modifier sans
risquer d'altérer considérablement la cohérence de l'individu.
Nous présenterons certaines de ces problématiques, puis proposerons
plusieurs solutions que nous comparerons et expliquerons.
MARKOV
* Vérification du locuteur -- Charles-Alban Deledalle
La vérification du locuteur consiste à détecter si un segment de parole
est réellement prononcé par un individu présumé. Cela est mis en
opposition à l'identification dont le but est de reconnaître l'auteur du
message.
Au cours de ce séminaire nous examinerons trois approches. La première
approche, probabiliste (état de l'art), utilise les modèles de mixture
gaussienne. Puis nous proposerons deux solutions basées sur les méthodes
SVM. La différence entre ces deux dernières se situe au niveau des
noyaux et des caractéristiques utilisés.
Notre travail s'inscrit dans le prolongement de l'évaluation NIST, et
dans le cadre de l'évaluation ISCSLP en cours.
* Model-checking qualitatif approché -- Jean-Philippe Garcia Ballester
Le model-checking consiste à vérifier certaines propriétés sur un modèle
donné. Il existe plusieurs méthodes pour résoudre ce problème, dont une
méthode approchée, permettant de réduire le temps de calcul.
Cette méthode est quantitative : ce qui nous intéresse est la
probabilité que la formule soit vraie. Mais il y a des cas où le
qualitatif est suffisant : ce qui nous intéresse est de savoir si cette
probabilité est supérieure ou inférieure à un certain seuil.
Nous présenterons d'abord le model-checking, et l'algorithme implémenté
dans APMC, puis une optimisation de celui-ci dans le cas de la
vérification qualitative de propriétés. Nous finirons par des tests,
théoriques et expérimentaux.
* Chaînes de Markov continues en présence d'incertitudes -- Nicolas Neri
Le 26 Mars 2006 lors de la 12e conférence internationale TACAS, Khoushik
SEN et al. ont présenté un article sur la vérification de programmes en
utilisant les chaînes de Markov finies à temps discret pour lesquelles
la probabilité exacte des transitions n'est pas connue.
Ce séminaire présentera les travaux en cours sur l'extension de
l'algorithme de Khoushik SEN et al. pour les chaînes de Markov à temps
continu présentant des incertitudes. Le but sera de trouver un ensemble
de variables satisfaisant certaines contraintes et de vérifier la
faisabilité de celles-ci grâce à la résolution des BMIs.
--
Daniela Becker
