This thesis develops a verification theory for systems of parallel processes communicating with one another by sending messages. The goal is independent specification of processes in a system, so that the system can be verified from the specifications of its component processes. A process is regarded as a generator of a formal language called its communication language. A specification is written as a first order predicate calculus formula about this formal language. Processes are verified by including assertions in them and proving that the assertions hold, much as is done for sequential programs. An important aspect of the work is its treatment of non-determinism and its effect on the termination, non-termination, and deadlock properties of systems and processes. It is argued that non-determinism should be curtailed if specifications are to accurately reflect the specifier's wishes. Rules relating assertions and statements are similar to those used in Floyd-Hoare logic. However, we deal here with both partial correctness, sometimes called safety in the literature, and liveness, which is a concept analgous to termination of sequential programs. Justification of liveness assertions takes advantage of statements that occur both before and after the assertion, introducing a new kind of proof rule which we prove is correct.