Symbolic Execution of MPI Programs with One-Sided Communications

Message-passing interface (MPI) programs are non-deterministic and challenging to ensure correctness. The introduction of one-sided communications makes the problem of non-determinism more severe for MPI programs. This paper reports our in-progress work of symbolic execution for the MPI programs with one-sided communications. Our approach can cover the non-determinism caused by the inputs, one-sided communication, and message-passing operations of MPI programs. The preliminary evaluation's results indicate the promising of our approach.