I..Vernier Symbolic Executions of Symmetrical Parallel Programs Nous proposons un algorithme pour exécuter symboliquement des programmes parallèles définis pour un nombre fini mais non déterminé de processus. Habituellement, on instancie les pro­ grammes avant de les exécuter; le nombre de processus est fixé. Nous exploitons le comportement symétrique des processus pour exécuter simultanément tous les programmes instanciés. Nous définissons des états symboliques qui représentent des ensembles d'états d'un nombre infini de programmes instanciés. Nous calcu­ lons simultanément tous les successeurs des états représentés pas un état symbolique. Après une exécution exhaustive, nous constru­ isons un graphe qui représente tous les états accessibles et exécutions possibles des programmes instanciés. Nous pouvons ex­ plorer ce graphe symbolique pour vérifier des propriétés ex­ primées par des formules de logique temporelle. We propose an algorithm to execute symbolically parallel pro­ grams with an unknown number of processes. Usually one instanti­ ates 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 pro­ grams. We define symbolic states that represent sets of states of an infinite number of instantiated programs. We compute si­ multaneously all the successors of states represented by a sym­ bolic 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.