Message-passing parallelism is widely used in High Performance
Computing (HPC), and will continue to be used in the foreseeable
future.  HPC applications perform complex and expensive computations
that are of fundamental importance for science, engineering, and
society.  It is therefore critical that these programs are
\emph{correct}, and effective methods for verifying the correctness of
message-passing programs are needed.

This dissertation presents a new method for specifying and verifying
correctness of message-passing programs.  The method is based on
procedure contracts.  These provide a natural and intuitive way to
decompose the specification and verification tasks.

While procedure contracts have been widely-studied for sequential
programs, it is not obvious how to generalize them for message-passing
parallel programs.  The approach presented here is based on the notion
of \emph{collective contract}, which is analogous to the notion of
\emph{collective function} in message-passing programming.
  
The first contribution of this dissertation is a rigorous theory of
collective contracts, presented using a ``toy'' message-passing
language.  Second, we present an automated approach for verifying such
contracts, given a bound on the number of processes, using model
checking and symbolic execution techniques.  Our third contribution is
a specification language for C/MPI programs, which deals with many of
the complexities of those languages.  Finally, we have implemented a
verifier for specified C/MPI programs using a general verification
framework, CIVL.  This system is evaluated with a number of simple,
but realistic, C/MPI programs.