Analysis of MPI Programs

We investigate the application of formal verification techniques to parallel programs that employ the Message Passing Interface (MPI). We develop a formal model of a subset of MPI, and then prove a number of theorems about that model that ameliorate or eliminate altogether the state explosion problem. As an example, we show that if one wishes to verify freedom from deadlock, it suffices to consider only synchronous executions.

@TechReport{siegel-avrunin:2004:mpi_tr,
  author = "Stephen F. Siegel and George S. Avrunin"
  title = "Analysis of {MPI} Programs"
  institution = "Department of Computer Science, University of Massachusetts",
  year = 2003,
  number = "UM-CS-2003-36"
}