Frédéric GAVA (MCf, responsable du projet)   Equipe : Systèmes communicants du LACL Page perso et courriel Thèmes de recherche : Mon travail au LACL consiste à fournir des outils (sémantiques, algorithmes, implantations correctes) permettant la portabilité, la sûreté et la certification des composantes d'une bibliothèque dédiée à la programmation parallèle de haut-niveau (appelé BSMLlib) ainsi que de l'étendre dans un environnement de méta-computing. Cette bibliothèque permet de programmer de manière fonctionnelle des algorithmes BSP (Bulk Synchronous Parallelism), un modèle de parallélisme permettant la prévision des performances sur une grande variété d'architectures. Plus récemment, mes travaux ont évolué vers les problématiques de vérification parallèle de l'algèbre M-Net. Frédéric LOULERGUE (Pr)   Equipe : Parallélisme Réalité virtuelle et Vérification de système (PRV) du LIFO Page perso et courriel Thèmes de recherche : Les activités menées au LIFO autour de la programmation de haut-niveau pour les architectures parallèles, distribuées et globalisées suivent deux grands axes. Le premier traite de la conception de langages et bibliothèques de haut-niveau, basés sur des sémantiques formelles, et le développement d'applications avec ces langages et bibliothèques. Le second traite de la vérification de programmes parallèles de haut-niveau : preuves de programmes parallèles, correction des compilateurs et des machines virtuelles associées à nos langages, outils d'analyse statique. Franck POMMEREAU (MCf)   Equipe : Systèmes communicants du LACL Page perso et courriel Thèmes de recherche : Mes travaux de recherche portent sur des modèles structurés explicitant la concurrence et qui s'appliquent au domaine du temps-réel. J'ai notamment développé une représentation du temps et de la préemption dans le cadre d'une algèbre de réseaux de Petri colorés (algèbre des M-Nets). Ces travaux ont été appliqués à la vérification des systèmes temps-réel et à la sémantique des langages de programmation parallèles ou concurrents. Plus récemment, mes travaux ont évolué vers les problématiques d'exécution et de vérification efficaces de ce formalisme. Mostafa BAMHA (MCf)   Equipe : Parallélisme Réalité virtuelle et Vérification de système (PRV) du LIFO Page perso et courriel Thèmes de recherche : Mes travaux de recherche sur le domaine des bases de données parallèles ont pour objectif la mise en place d'un prototype de système de gestion de bases de données sur une architecture GRID traitant de manière efficace les problèmes de déséquilibre des données et des charges des différents processeurs tout en optimisant l'allocation des ressources de l'architecture parallèle utilisée. Elisabeth Pelz (Pr, associé au projet)   Equipe : Systèmes communicants du LACL Page perso et courriel Thèmes de recherche : M-Net, S-Net, sécurité informatique, vérification, Réseaux de Petri Gaétan HAINS (Pr, associé au projet)   Equipe : Systèmes communicants du LACL Page perso et courriel Thèmes de recherche : Mes recherches portent sur la programmation parallèle de haut-niveau : portabilité des performances (modèle BSP), outils de programmation et conception d'algorithmes pour le re-balancement des données dirigés pour les coûts parallèles BSP avec notamment des applications aux solveurs de contraintes, à l'apprentissage automatique aux bases de données et à la bio-informatique. Je m'intéresse aussi à la démonstration automatique appliquée à la vérification de sûreté du logiciel et des protocoles cryptographiques (dans le cadre du projet SATIN de l'ACI). J'ai participé/coordonné plusieurs projets dans ces domaines. Jean-Michel COUVREUR (Pr, associé au projet)   Equipe : Parallélisme Réalité virtuelle et Vérification de système (PRV) du LIFO Page perso et courriel Thèmes de recherche : Dans le cadre de mes recherches, j'ai travailler sur l'amélioration de trois aspects de l'algorithmique de la vérification (notamment des réseaux de Petri) : la logique temporelle linéaire (LTL), la vérification par ordre partiel et la vérification symbolique. La logique LTL permet de maîtriser l'explosion du nombre d'états et ceci grâce aux techniques de réduction par ordre partiel (par exemple les techniques de dépliage). J'ai aussi participer à l'enrichissement des techniques de vérification symbolique avec des résultats de décidabilité pour les systèmes infinis grâce à des présentations plus fines des données comme par exemple les Diagrammes de Décisions de Données. Doctorants   Equipe "Systèmes communicants" du LACL : Louis GESBERT (Page perso et courriel) Equipe "Parallélisme Réalité virtuelle et Vérification de système (PRV)" du LIFO : Radia BENHEDDI (Page perso et courriel) MohamadS AL HAJJ HASSAN (courriel) Duy Tung NGUYEN (Page perso et courriel)