Abstract. 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.Stephen F. Siegel and George S. Avrunin, Modeling Wildcard-Free MPI Programs for Verification, in Proceedings of the ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming, pages 95-106, Chicago, IL, June 2005.
You may download the paper in one of the following formats: