VSL | Publications | Modeling Wildcard-free MPI Programs for Verification

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