Abstract FR:

Le calcul massivement parallele a connu durant ces deux dernieres decennies un fort developpement. Les efforts dans ce domaine ont d'abord surtout ete orientes vers les machines, plutot qu'a la definition de langages adaptes au parallelisme massif. Par la suite, deux principaux modeles de programmation ont emerge : le parallelisme de controle et le parallelisme de donnees. Le premier a connu un vif succes. Dans ce modele cependant, les applications massivement paralleles s'averent difficiles a concevoir et peu fiables, compte tenu du grand nombre de processus envisages. En revanche, le parallelisme de donnees parait aujourd'hui etre un bon compromis entre les besoins des utilisateurs et les contraintes imposees par les architectures paralleles. Dans cette these, nous nous sommes interesse a la validation formelle des langages a parallelisme de donnees. L'idee est de tirer parti de la relative simplicite de ce modele de programmation pour developper des methodes semblables a celles deja eprouvees dans le cadre des langages scalaires classiques. La premiere partie du travail effectue concerne un langage data-parallele simple, de type imperatif. Nous avons montre qu'il etait possible de definir un systeme de preuve complet pour ce langage, inpire de la logique de hoare. L'etude theorique nous a permis en outre de definir une methodologie pratique de preuve par annotations, semblable a celle utilisee pour les langages scalaires. Nous nous sommes ensuite tourne vers le langage d'equations recurrentes alpha. Il s'averait necessaire de definir pour ce langage un cadre formel de validation, plus riche que le systeme de transformations existant ne permettant que des preuves par equivalence. Nous avons defini un modele d'execution par l'intermediaire d'une semantique operationnelle, et une methodologie de preuve. Celle-ci utilise des invariants qui sont raffines a partir d'une traduction du programme dans un langage logique jusqu'a l'obtention de la propriete voulue.