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.
Please feel free to contact us if you have any problem.
[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). (Pre-print)