  The Message Passing Interface (MPI) is the de facto standard message-passing
infrastructure for developing parallel applications. Two decades after the
first version of the library specification, MPI-based applications are nowadays
routinely deployed on super and cluster computers. These applications, written
in C or Fortran, exhibit intricate message passing behaviours, making it hard
to statically verify important properties such as the absence of deadlocks. Our
work builds on session types, a theory for describing protocols that provides
for correct-by-construction guarantees in this regard. We annotate MPI
primitives and C code with session type contracts, written in the language of a
software verifier for C. Annotated code is then checked for correctness with
the software verifier. We present preliminary results and discuss the
challenges that lie ahead for verifying realistic MPI program compliance
against session types.
