ABSTRACT. The success of dynamic verification techniques for C MPI (Message Passing Interface) programs rest on their ability to address communication non-determinism. As the number of processes in the pro- gram grows, the dynamic verification techniques suffer from the problem of an exponential growth in the size of the reachable state space. In this work, we provide a hybrid verification technique that combines explicit- state dynamic verification with symbolic analysis of message passing pro- grams. The dynamic verification component deterministically replays the execution runs of the program, while the symbolic component encodes a set of interleavings of the observed run of the program in a quantifier-free first order logic formula and verifies the formula for property violations such as assertions and absence of communication deadlocks. In the ab- sence of property violations, it performs analysis to generate a different run of the program that does not fall in the set of already verified runs of the program. We demonstrate the effectiveness of our methodology by our prototype tool Hermes. Our evaluation indicates that for non-single- path MPI programs, the verification time reduces by at least 3 times when Hermes is compared against the state-of-the-art verification tools.