Abstract. 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.This paper appeared as Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts, 2003.
You may download the paper in one of the following formats:
Other items: