Modeling wildcard-free MPI programs for verification
Stephen F. Siegel, George S. Avrunin · 2005
We give several theorems that can be used to substantially reduce the state space that must be considered in applying finite-state verification techniques, such as model checking, to parallel programs written using a subset of MPI. We illustrate the utility of these theorems by applying them to a small but realistic example.