Symbolic executions of symmetrical parallel programs

We propose an algorithm to execute symbolically parallel programs with an unknown number of processes. Usually one instantiates the programs before their execution, i.e., one fixes the number of processes. We exploit the symmetrical behaviors of the processes to execute simultaneously all the instantiated programs. We define symbolic states that represent sets of states of an infinite number of instantiated programs. We compute simultaneously all the successors of states represented by a symbolic one. After an exhaustive execution, we build a graph that represents all the reachable states and possible executions of the instantiated programs. We can explore this symbolic graph to verify properties expressed with temporal logic formulas