G.S.: Analysis of MPI programs

Abstract. We investigate the application of formal verification techniques to parallel programs which 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 which 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. 1