To examine our contract-based verification approach for
message-passing, we implemented a prototype for real-world MPI
programs.  

Compare to \minimp{}, MPI programs are much more complicated in that
1) there are hundreds of functions, data types and constants defined
in MPI libraries; and 2) client programming languages of MPI
libraries, C/C++ and Fortran, are error-prone.

Our implementation is based on a mature verification framework, CIVL,
which was designed for verifying general concurrent programs.  The
CIVL framework is flexible enough for developers to customize it for
dealing with specific kinds of concurrency APIs.  The author of this
dissertation is one of the main developers that built the support of
C/MPI in CIVL.  The contract system is then built on top of this MPI
support for only C programs.

In this chapter, we give a brief introduction for CIVL and its MPI
support, which serve as the background of the contract system
implementation.  An overview of CIVL is given in \S\ref{sec:civl} and
a description of the MPI support is presented in
\S\ref{sec:civl:mpi-support}.  More details of CIVL can be found in
\cite{siegel-etal:2015:civl_sc}.  The work of verifying MPI programs
using CIVL in a monolithic way is published
as \cite{Luo:2017:VMP:3127024.3127032}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%