Friedrich' theory of symmetric positive systems of first-order PDE's is revisited so as to avoid invoking traces at the boundary. Two intrinsic geometric conditions are introduced to characterize admissible boundary conditions. It is shown that the space in which admissible boundary conditions can be enforced is maximal in a positive cone associated with the differential operator. The equivalence with a formalism based on boundary operators is investigated and practical means to construct these boundary operators are presented. Finally, the link with Friedrich' formalism and applications to various PDE's are discussed.

We study the serial correctness of programs in a subset of Fortran X3H5, a control-parallel extension of Fortran. This property, an equivalence between a parallel program and its sequential version, follows from the preservation of dependences, defined on the sequential version, by the control flow and the synchronizations. To check this preservation, we propose an algorithm which builds a formula, using a new kind of block graph. Under a linearity assumption, the algorithm tries to prove that this formula is a tautology by means of the Omega test.

We study a property of correctness of programs written. in a shared-memory parallel language. This property is a semantic equivalence between the parallel program and its sequential version, that we define: We consider some standard parallel imperative language. Within this language, this correctness property follows from the preservation of data dependences by the control flow and the synchronizations. Our result makes use of the semantics of the sequential version only. Hence, through our result, checking the correctness of some parallel program boils down to verifying properties of some sequential program.

Nous etudions une propriete de correction de programmes ecrits dans un langage parallele. Cette propriete est une equivalence semantique entre le programme parallele et sa version sequentielle, que nous definissons. Le langage que nous considerons, outre des structures sequentielles usuelles (boucles, branchements conditionnels), comporte des boucles paralleles et des synchronisations par evenements. L'objet principal de cette these est de demontrer un theoreme qui assure cette propriete de correction, sous un certain nombre d'hypotheses, principalement une condition de preservation des dependances de donnees. Ces hypotheses portent seulement sur la semantique de la version sequentielle : autrement dit, en vertu de notre resultat, verifier la correction d'un certain programme parallele se ramene a verifier un certain nombre de proprietes de sa seule version sequentielle. Par ailleurs, nous esquissons une extension de ce resultat, par l'introduction de sections critiques, envisageant alors une version affaiblie (c'est-a-dire generalisee) de notre propriete de correction. (Resume de l'auteur).