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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Siegel, S. F., & Rossi, L. F. (2008). Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5205 LNCS, pp. 274–282). https://doi.org/10.1007/978-3-540-87475-1_37
Mendeley helps you to discover research relevant for your work.