Model Checking Nonblocking MPI Programs

DOI10.1007/978-3-540-69738-1_3MaRDI QIDQ5452594zbMATH OpenOpenAlexFDO

Authors Stephen F. Siegel

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69738-1_3

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Deadlock detection in MPI programs
• Symbolic verification of MPI programs with non-deterministic synchronizations
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Software
• MPI-CHECK: a tool for checking Fortran 90 MPI programs

Cites work

• Model Checking Software

Cited in

(17)

• TASS: the toolkit for accurate scientific software
• Dynamic symbolic verification of MPI programs
• Symbolic verification of MPI programs with non-deterministic synchronizations
• State-space reduction of non-deterministically synchronizing systems applicable to deadlock detection in MPI
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Collective assertions
• Specification and verification of a MPI implementation for a MP-SoC
• Memory debugging of MPI-parallel applications in Open MPI
• scientific article; zbMATH DE number 1285209 (Why is no real title available?)
• scientific article; zbMATH DE number 1455629 (Why is no real title available?)
• scientific article; zbMATH DE number 2087631 (Why is no real title available?)
• MPI-CHECK: a tool for checking Fortran 90 MPI programs
• Model Checking Software
• Verification, Model Checking, and Abstract Interpretation
• A Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI Programs
• Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API
• MPI correctness checking for OpenMP/MPI applications

This page was built for publication: Model Checking Nonblocking MPI Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452594)