Combining Symbolic Execution and Model Checking to Verify MPI Programs