English

Verification of MPI programs

Logic in Computer Science 2021-10-19 v1 Programming Languages
Authors: Andrew M. Mironov
View on arXiv ↗ PDF ↗

Abstract

In this paper, we outline an approach to verifying parallel programs. A new mathematical model of parallel programs is introduced. The introduced model is illustrated by the verification of the matrix multiplication MPI program.

Keywords

formal verification

Cite

@article{arxiv.2110.08537,
  title  = {Verification of MPI programs},
  author = {Andrew M. Mironov},
  journal= {arXiv preprint arXiv:2110.08537},
  year   = {2021}
}

Related papers

View all related →
Programming Languages · Computer Science
Deductive Verification of Parallel Programs Using Why3
César Santos, Francisco Martins, Vasco Thudichum Vasconcelos
2015-08-21
Logic in Computer Science · Computer Science
Methods to Model-Check Parallel Systems Software
Olga Shumsky Matlin, William McCune, Ewing Lusk
2007-05-23
Programming Languages · Computer Science
Inferring Types for Parallel Programs
Francisco Martins, Vasco Thudichum Vasconcelos, Hans Hüttel
2017-04-12
Programming Languages · Computer Science
Practical Formal Verification for MLIR Programs
Emily Tucker, Louis-Noël Pouchet, Erika Hunhoff, Stephen Neuendorffer +1
2026-05-05
Logic in Computer Science · Computer Science
From Matching Logic To Parallel Imperative Language Verification
ShangBei Wang
2021-02-09
Programming Languages · Computer Science
A Quick Introduction to Functional Verification of Array-Intensive Programs
Kunal Banerjee, Chandan Karfa
2019-05-23
Numerical Analysis · Mathematics
Parallel Computation of functions of matrices and their action on vectors
Sergio Blanes
2022-10-10
Distributed, Parallel, and Cluster Computing · Computer Science
Towards deductive verification of MPI programs against session types
Eduardo R. B. Marques, Francisco Martins, Vasco T. Vasconcelos, Nicholas Ng +1
2013-12-11
Programming Languages · Computer Science
To parallelize or not to parallelize, bugs issue
Alaa I. El-Nashar, Nakamura Masaki
2013-11-05
Mathematical Software · Computer Science
Program Verification of Numerical Computation
Garry Pantelis
2014-01-08
Programming Languages · Computer Science
Combining Symbolic Execution and Model Checking to Verify MPI Programs
Hengbiao Yu, Zhenbang Chen, Xianjin Fu, Ji Wang +4
2020-01-20
Distributed, Parallel, and Cluster Computing · Computer Science
Parallel Implementations of the Jacobi Linear Algebraic Systems Solve
Athanasios Margaris, Stauros Souravlas, Manos Roumeliotis
2014-03-27
Software Engineering · Computer Science
Verifying Parallel Loops with Separation Logic
Stefan Blom, Saeed Darabi, Marieke Huisman
2014-06-16
Programming Languages · Computer Science
Proving Correctness of Parallel Implementations of Transition System Specifications
Frank S. de Boer, Einar Broch Johnsen, Violet Ka I Pun, Silvia Lizeth Tapia Tarifa
2023-02-10
Programming Languages · Computer Science
Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)
Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Lars Nitzke
2023-11-03
Programming Languages · Computer Science
To parallelize or not to parallelize, control and data flow issue
Alaa I. Elnashar
2013-11-05
Software Engineering · Computer Science
Control Explicit---Data Symbolic Model Checking: An Introduction
Jiri Barnat, Petr Bauch
2013-04-01
Distributed, Parallel, and Cluster Computing · Computer Science
MPI Errors Detection using GNN Embedding and Vector Embedding over LLVM IR
Jad El Karchi, Hanze Chen, Ali TehraniJamsaz, Ali Jannesari +2
2024-03-06
Programming Languages · Computer Science
Two automated techniques for analyzing and debugging Mpi-based programs
Alaa Ismail Elnashar, Sultan Aljahdali, Mosaid Al Sadhan
2013-11-06
Logic in Computer Science · Computer Science
A Formal Model For Real-Time Parallel Computation
Peter Hui, Satish Chikkagoudar
2013-01-03
Astrophysics · Physics
Parallel Programming with MatlabMPI
Jeremy Kepner
2007-05-23
Software Engineering · Computer Science
Verification of Concurrent Engineering Software Using CSM Models
Jerzy Mieścicki, Mikołaj Baszun, Wiktor B. Daszczuk, Bogdan D. Czejdo
2017-04-24
Distributed, Parallel, and Cluster Computing · Computer Science
MPISE: Symbolic Execution of MPI Programs
Xianjin Fu, Zhenbang Chen, Yufeng Zhang, Chun Huang +2
2014-09-16
Programming Languages · Computer Science
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Aleksandr Fedchin, Antero Mejr, Hari Sundar, Jeffrey S. Foster
2025-12-23
Logic in Computer Science · Computer Science
SPINning Parallel Systems Software
O. S. Matlin, E. Lusk, W. McCune
2007-05-23
R2 v1 2026-06-24T06:56:26.606Z