Dynamic symbolic verification of MPI programs

DOI10.1007/978-3-319-95582-7_28MaRDI QIDQ2024366zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(11)

• MPI-CHECK: a tool for checking Fortran 90 MPI programs
• Unfolding-based dynamic partial order reduction of asynchronous distributed programs
• Collective assertions
• Symbolic verification of MPI programs with non-deterministic synchronizations
• Going beyond dual execution: MPC for functions with efficient verification
• Model Checking Software
• 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
• System-level state equality detection for the formal dynamic verification of legacy distributed applications

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)