4th Euromicro Workshop on Parallel and Distributed Processing (PDP '96) Symbolic Executions of Symmetrical Parallel Programs PORTUGAL January 24-January 26 ISBN: 0-8186-7376-1
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.
Index Terms:
Petri net, symbolic execution, parameterized programs
Citation:
Isabelle Vernier, "Symbolic Executions of Symmetrical Parallel Programs," pdp, pp.0327, 4th Euromicro Workshop on Parallel and Distributed Processing (PDP '96), 1996 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||