Concurrent processes can exhibit extremely complicated behavior, and neither informal reasoning nor testing is reliable enough to establish their correctness. In this thesis, we develop a new technique for the verification of parallel programs. The technique is stated in terms of axioms and inference rules, and it is used to prove safety and liveness properties of parallel programs. Safety properties are assertions that must be satisfied by the system state at all times; they are analogous to partial correctness. Liveness properties refer to events that will occur in the future, such as program termination or the eventual receipt of a message. In addition to the formal proof rules, we present several heuristics to aid in the preparation of correctness proofs.

We model a parallel program as a set of interacting modules (processes and monitors), and we exploit this modularity in the verification process. First we prove properties of the low-level modules directly from their code. We then combine the specifications of the low-level modules to prove properties of higher-level modules, without again referring to the code. Eventually, we prove properties of the entire program.

We discuss the application of this verification technique to two classes of parallel programs: network protocols and resource allocators. Most previous approaches to verifying network protocols have been based upon reachability arguments for finite-state models of the protocols. Only protocols of limited complexity can be verified using the finite-state model, because of the com- binatorial explosion of the state space as the complexity of the protocol in- creases. In contrast, our approach allows us to abstract information from the details of the implementation, so that the proof need not grow unmanageably as the protocol size increases.

The discussion of resource allocation centers around Hoare's structured paging system, which is a complex hierarchical program. With this example, we demonstrate that many of the techniques used in program verification can be used for specification as well.

The thesis also describes a number of tools that have been useful in proving concurrent programs. Two of the most important are history variables and temporal logic. We employ history variables to record the interaction between the modules that constitute a program. Temporal logic serves as a convenient notation for stating and proving liveness properties.