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.
https://hal.inria.fr/inria-00073660
Contributeur : Rapport de Recherche Inria
<>
Soumis le : mercredi 24 mai 2006 - 13:26:12
Dernière modification le : jeudi 17 janvier 2019 - 15:06:04
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:22:00
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〉
