Seminar/2008-05-28

Mercredi 28 mai 2008, 14h-17h, Amphi 4

Le langage BSML

Documents

gava.pdf

Frédéric Gava, LACL, Université de Paris Est, Créteil

Nous présenterons BSML (Bulk Synchronous Parallel ML), un langage de programmation de haut-niveau pour machines parallèles, ainsi que des exemples classiques de parallélisme implémentés dans ce langage. Nous complèterons cette présentation par une étude comparative des coûts théoriques de ces algorithmes réalisée sur la grappe de PC du LACL.

Frédéric Gava est maître de conférences en informatique à l'université de Paris 12. Ses travaux de thèse ont porté sur la programmation parallèle (et des méta-ordinateurs) de haut-niveau qui lui ont valu le prix de thèse 2006 de la fondation EADS dans le domaine des STIC. Il travaille actuellement sur la preuve de programme parallèle et la conception d'un vérificateur parallèle de modèles pour réseaux de Petri de haut-niveau implanté avec les méthodes développées lors de son travail de thèse.

http://lacl.univ-paris12.fr/gava/

Programmation parallèle certifiée

Frédéric Loulergue, LIFO, Université d'Orléans

L'algorithmique constructive permet, partant d'une spécification écrite sous forme d'une combinaison non-efficace de fonctions, de dériver, sous certaines conditions, des algorithmes parallèles efficaces. Cette dérivation s'appuie sur des théorèmes d'équivalence de programmes et est formellement correcte. Elle aide le programmeur à concevoir des programmes parallèles. Toutefois les bibliothèques de squelettes proposées ne sont pas certifiées. Dans le cadre d'une collaboration avec l'université de Tokyo, nous proposons de cibler des squelettes algorithmiques développés en BSML et certifiés à l'aide de l'assistant de preuve Coq.

Frédéric Loulergue est professeur à l'Université d'Orléans depuis septembre 2005, directeur adjoint du Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), membre de l'équipe Parallélisme, Réalité virtuelle et Vérification (PRV). Il travaille sur le parallélisme avec des langages et modèles de haut-niveau (conception de langages et bibliothèques, sémantique, vérification, algorithmes et applications).

http://f.loulergue.free.fr/