Formal Validation of Data-Parallel Programs : a Two-Component Assertional Proof System for a Simple Language

Abstract : We present a proof system for a simple data-parallel kernel language called \L. This proof system is based on a two-component assertion language. We define a weakest preconditions calculus and analyse its definability properties. This calculus is used to prove the completeness of the proof system. We also present a two-phase proof methodology, yielding proofs similar to those for scalar languages. We finally discuss other approaches.
Type de document :
Rapport
[Research Report] RR-3033, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073660
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:26:12
Dernière modification le : vendredi 20 avril 2018 - 15:44:24
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:22:00

Fichiers

Identifiants

  • HAL Id : inria-00073660, version 1

Citation

Luc Bougé, David Cachera, Yann Le Guyadec, Gil Utard, Bernard Virot. Formal Validation of Data-Parallel Programs : a Two-Component Assertional Proof System for a Simple Language. [Research Report] RR-3033, INRIA. 1996. 〈inria-00073660〉

Partager

Métriques

Consultations de la notice

455

Téléchargements de fichiers

291