# Combining Symbolic Execution and Model Checking to Verify MPI Programs

## TL;DR

This paper introduces MPI-SV, a novel tool that combines symbolic execution and model checking to efficiently verify MPI programs, especially those with non-blocking operations, significantly improving scalability and verification success rate.

## Contribution

The paper presents MPI-SV, the first symbolic execution based verifier for MPI programs with non-blocking operations, integrating symbolic execution and model checking for enhanced verification capabilities.

## Key findings

- MPI-SV verifies 90% of tasks compared to 55% by pure symbolic execution.
- MPI-SV achieves 19x speedup in verifying properties.
- MPI-SV verifies 100 tasks within one hour, outperforming previous methods.

## Abstract

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV (footnote: https://mpi-sv.github.io) and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55\%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90\%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.