Systematic Parallel Programming

reasoning, trace semantics. Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety ofvery di erent parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This thesis addresses some of these problems by developing a formal basis for the design of parallel programs in form of a re nement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level speci cation. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the re nement tree. Development e orts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly mor