Dynamic symbolic verification of MPI programs

DOI10.1007/978-3-319-95582-7_28zbMATH Open1460.68029OpenAlexW2808769940MaRDI QIDQ2024366FDOQ2024366

Authors: Dhriti Khanna, Subodh Sharma, César Rodríguez, Rahul Purandare 

Publication date: 4 May 2021

Full work available at URL: https://doi.org/10.1007/978-3-319-95582-7_28

Recommendations

• Symbolic verification of MPI programs with non-deterministic synchronizations
• Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
• A sound reduction of persistent-sets for deadlock detection in MPI applications
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Nonblocking MPI Programs

zbMATH Keywords

deadlock detectionsymbolic analysismessage-passing interfacedynamic verification

Mathematics Subject Classification ID

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

Cites Work

• TASS: the toolkit for accurate scientific software
• A high-performance, portable implementation of the MPI message passing interface standard
• Verification, Model Checking, and Abstract Interpretation
• Software verification for weak memory via program transformation
• Trace-based symbolic analysis for atomicity violations
• Symbolic predictive analysis for concurrent programs
• Deadlock detection in MPI programs
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• State-space reduction of non-deterministically synchronizing systems applicable to deadlock detection in MPI
• Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings

Cited In (9)

• MPI-CHECK: a tool for checking Fortran 90 MPI programs
• Unfolding-based dynamic partial order reduction of asynchronous distributed programs
• Collective assertions
• Model Checking Software
• Going beyond dual execution: MPC for functions with efficient verification
• Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
• Verification, Model Checking, and Abstract Interpretation
• A sound reduction of persistent-sets for deadlock detection in MPI applications
• Verifying parallel programs with dynamic communication structures

This page was built for publication: Dynamic symbolic verification of MPI programs

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