Réalisations du responsable dans le domaine de l’UE
-
Production de documents interactifs (XML) pour un système de formation basé sur simulateur : O. Auzende, M. Joab, F. Rivière, P. Le Leydour, M. Futtersack, A knowledge-based generator for After Action Review interactive documents, CALIE'04, Grenoble, 2004.
-
Réalisation d'un système de commande de manuels via le Web (PHP, mySQL) pour le site de la bibliothèque universitaire (Paris 2), 2005.
-
Elaboration des supports en ligne pour la formation au C2i (Paris 2, Paris 3), 2005.
-
Réalisation d'une maquette (PHP, mySQL) de réactualisation du logiciel AUTOEVAL pour l'UTES (Paris 6), 2005.
Acronyme : inabs
|
Spécialité : STL
|
3 ECTS
|
Niveau : 500
|
Semestre : S3
|
Titre : Interprétation abstraite
|
Responsable : Mathieu JAUME
| Répartition hebdomadaire ou semestrielle |
(CM: 2h00)(TD: 1h00)(TME: 0h00)
| Contenu
Cette U.E. vise a introduire, au travers d'exemples, les techniques de base de l'analyse statique par interprétation abstraite.
| Expérience du responsable dans le domaine de l’UE
Mes thèmes de recherche s'articulent autour de la définition de sémantiques formelles et de l'utilisation de ces sémantiques pour garantir (par la preuve) des propriétés de programmes, notamment dans le domaine de la sécurité (controle d'accès). L'analyse statique par interprétation abstraite s'inscrit dans ce thème puisque les techniques mises en oeuvre reposent sur la definition d'une sémantique abstraite prouvée correcte par rapport à la sémantique concrète.
| Réalisations du responsable dans le domaine de l’UE
-
Co-encadrement de la thèse de Thibault Chevalier Names : "Analyse statique de code JavaCard" (thèse CIFRE - Oberthur) . En cours.
-
With Charles Morisset. Formalisation and Implementation of Access control models, Information Assurance and Security IAS, International Conference on Information Technology ITCC'2005, Las Vegas, NV USA, pp 703-708, IEEE CS Press, 2005.
-
With Virgile Prevosto. Making proofs in a hierarchy of mathematical structures, Calculemus 2003, 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2003.
-
On greatest fixpoint semantics of logic programming, Journal of Logic and Computation, 12 (2):321-342,2002.
-
With David Delahaye and Virgile Prevosto. Coq : un outil pour l'enseignement, To appear, Technique et Science Informatique, TSI, 2005
|
Acronyme : indus
|
Spécialité : ACSI
|
3 ECTS
|
Niveau : 500
|
Semestre : S4
|
Titre : Chaînes de CAO industrielles (Commercial CAD tools)
|
Responsable : Roselyne CHOTIN-AVOT
| Répartition hebdomadaire ou semestrielle |
(TD/TME: 4h00)
| Contenu
Module à vocation professionnalisante : formation pratique aux outils CAO/VLSI utilisés dans l'industrie
| Expérience du responsable dans le domaine de l’UE
Dans le cadre de mes recherches, je m'intéresse à la conception de chemins de données arithmétiques et à l'adéquation algorithme/architecture. Ce type de conception nécessite d'utiliser les chaînes de CAO industrielles.
| Réalisations du responsable dans le domaine de l’UE
-
Hardware implementation of discrete stochatic arithmetic, Roselyne Avot-Chotin et Habib Mehrez, Special Issuue of Numerical Algorithms, Kluwer Academic Publishers, janvier 2005
-
A floating-point unit using stochastic arithmetic compliant with the IEEE-754 standard, Roselyne Chotin et Habib Mehrez, 9th IEEE International Conference on Electronics, Circuits and Systems (ICECS 2002), Dubrovnik, Croatie, Septembre 2002, pp. 603-606
-
Use of Redundant Arithmetic on Architecture and Design of a High Performance DCT Macro-bloc Generator, Roselyne Chotin, Yannick Dumonteix et Habib Mehrez, 15th Design of Circuits and Integrated Systems Conference (DCIS 2000), Montpellier, France, Novembre 2000, pp. 428-433
|
Dostları ilə paylaş: |