Message Passing Interface (MPI) is the current de facto standard for developing the parallel applications in high-performance computing. However, developing MPI programs is challenging due to the non-determinism caused by parallel execution and complex programming features such as non-deterministic communications and asynchrony.

MPI-SV is an automatic symbolic verifier for verifying MPI C programs. MPI-SV supports the verification of non-blocking MPI programs. MPI-SV can verify the properties in Linear Temporal Logic (LTL).

The technique implemented by MPI-SV is presented in [1]. The technique combines symbolic execution and model checking in a synergistic manner to enlarge the scope of verifiable properties and improve the scalability of verification.

• Introduction

• Installation

• Manual

• Tutorial

• Docker Image

• Manual for the Docker Image

• Binary Github Repo

• Source Code Github Repo

Contacts

Please feel free to contact us if you have any problem.

• mpi.symbolic.verifier@gmail.com

[1]. Hengbiao Yu, Zhenbang Chen, Xianjin Fu, Ji Wang, Zhendong Su, Jun Sun, Chun Huang, Wei Dong. Symbolic Verification of Message Passing Interface Programs, in 42nd IEEE/ACM International Conference on Software Engineering (ICSE 2020). (PDF, Video)

[2]. Zhenbang Chen, Hengbiao Yu, Xianjin Fu, Ji Wang. MPI-SV: A Symbolic Verifier for MPI Programs, in 42nd IEEE/ACM International Conference on Software Engineering (ICSE 2020), Demo track. (PDF, Video)