Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les Actions de Recherche du LIFO > Action de Recherche : PROPAC

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37



PROPAC : Programmation Parallèle Certifiée

L'objectif de ce projet est de fournir un environnement de programmation permettant la production et l'exécution de programmes parallèles certifiés.

Plus techniquement, plusieurs axes complémentaires contribuent à l'objectif global de ce projet :

  • La preuve avec l'assistant de preuves Coq de programmes écrits dans les langages fonctionnels parallèles que nous avons développés.
  • La certification des compilateurs des langages que nous avons développés vers du code-octet pour des machines virtuelles adaptées et la certification partielle de ces machines virtuelles.
  • La preuve de programmes parallèles impératifs BSP (Bulk Synchronous Parallelism) écrits dans un mini-langage impératif dédié, puis écrits dans une extension de C ou Java.
  • La prévision de performance automatique des programmes écrits dans ces langages.

Financement

Ministère de la Recherche et des Nouvelles Technologies par le biais du Fonds National de la Science, programme ACI Jeunes Chercheurs et Chercheurs 2004 (projet de septembre 2004 à septembre 2007)

Participants

Radia BENHEDDI

Frédéric LOULERGUE

Page web de l'action

http://wwwpropac.free.fr/