Abstract
Ensuring the reliability of computer programs is particularly important, especially for systems with critical applications. The program correctness has to be verified to behave as they were intended to do. For parallel machines, the task is even more difficult because results of executing parallel programs can be very unpredictable as many processes are executed at the same time. A programmer is more likely to make mistakes. In this paper, methods to prove the correctness of parallel programs are proposed. They are based on the symbolic execution and the data dependence tests called the Bernstein Methods.