VSL | Publications | Analyzing BlobFlow

Stephen F. Siegel and Louis F. Rossi, Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software, Recent Advances in Parallel Virtual Machine and Message Passing Interface, 15th European PVM/MPI User's Group Meeting, Dublin, Ireland, September 7-10, 2008, Proceedings. Lecture Notes in Computer Science 5205, Springer-Verlag (2008), pages 274–282.

Model checking techniques are powerful tools for the analysis and verification of concurrent systems. This paper reports on a case study applying model checking techniques to a mature, MPI-based scientific program consisting of approximately 10K lines of code. The program, BlobFlow, implements a high order vortex method for solving the two-dimensional Navier-Stokes equations. Despite the complexity of the code, we verify properties including freedom from deadlock and the functional equivalence of sequential and parallel versions of the program. This has led to new insights into the technology that will be required to automate the modeling and verification process for complex scientific software.

@InProceedings{siegel-rossi:2008:eccsvm_pvmmpi,
  author = "Stephen F. Siegel and Louis F. Rossi",
  title = "Analyzing {BlobFlow}: A Case Study Using Model Checking to Verify Parallel Scientific Software",
  pages = {274--282},
  crossref = {pvmmpi2008}
}
@Proceedings{pvmmpi2008,
  booktitle = "Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings",
  title = "Recent Advances in {P}arallel {V}irtual {M}achine and {M}essage {P}assing {I}nterface, 15th {E}uropean {PVM/MPI} User's Group Meeting, Proceedings",
  publisher = "Springer",
  series = "LNCS",
  volume = {5205},
  year = {2008},
  editor = {Alexey Lastovetsky and Tahar Kechadi and Jack Dongarra},
  note = "To appear"
}