Using model checking with symbolic execution to verify parallel numerical programs