**Title:** Modeling Wildcard-free MPI Programs for Verification

**Authors:**
Stephen F. Siegel and
George S. Avrunin

**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.

**Appeared in:**

Proceedings of the ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming, pages 95-106, Chicago, IL, June 2005

**BibTeX:**

@InProceedings{siegel-avrunin:2005:ppopp, author = {Stephen F. Siegel and George S. Avrunin}, title = {Modeling Wildcard-free {MPI} Programs for Verification}, crossref = {ppopp2005}, pages = {95--106} } @Proceedings{ppopp2005, title = "Proceedings of the {ACM} {SIGPLAN} {S}ymposium on {P}rinciples and {P}ractice of {P}arallel {P}rogramming", booktitle = "Proceedings of the {ACM} {SIGPLAN} {S}ymposium on {P}rinciples and {P}ractice of {P}arallel {P}rogramming", year = 2005, address = "Chicago, IL", month = jun }

**Download:**

- mpi_ppopp_2005.pdf (full paper)
- mpi_ppopp_2005.tgz (Laplace examples used in paper)

VSL | Publications