Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.