ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 25/10 - 2006  - pp.1261-1280  - doi:10.3166/tsi.25.1621-1280
TITRE
Une bibliothèque certifiée de programmes fonctionnels BSP

RÉSUMÉ
Bulk-Synchronous Parallel ML ou BSML est un langage fonctionnel pour la programmation d'algorithmes BSP, un modèle qui permet la portabilité des programmes tout en offrant une prévision réaliste de leurs performances sur une grande variété d'architectures. BSML est basé sur une extension du langage ML par des opérations parallèles sur une structure de données appelée vecteur parallèle. Nous présentons ici le développement d'une bibliothèque de programmes BSML certifiée par l'assistant de preuves Coq. Cette bibliothèque pourra être utilisée pour le développement d'algorithmes BSP certifiés. Ce travail est un exemple de l'adéquation des logiques d'ordre supérieur au processus de certification et de correction d'applications parallèles.


ABSTRACT
The Bulk-Synchronous Parallel ML (BSML) is a functional language for BSP programming, a model of computing which allows parallel programs to be ported to a wide range of architectures. It is based on an extension of the ML language by parallel operations on a parallel data structure called parallel vector, which is given by intention. We present the certification of a library of BSML programs with the Coq proof assistant. This library could be used for the development of certified BSP algorithms. This development is an example of the usefulness of higher-order logic in the process of software certification of parallel applications.


AUTEUR(S)
Frédéric GAVA

MOTS-CLÉS
bibliothèque, certification, preuve, fonctionnel, Coq, BSP.

KEYWORDS
library, certification, proof, functional, Coq, BSP.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (186 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier