I. Vernier Symbolic Verification of Parallel Programs Nous proposons une solution partielle au problème de la vérification de propriétés de programmes parallèles avec un nom­ bre fini mais non déterminé de processus. Nous considérons une sous-classe des programmes représentés par les réseaux de Petri. L'originalité de notre méthode est de construire un graphe sym­ bolique. Les n.uds du graphe sont des prédicats qui représentent des ensembles d'états. Les propriétés exprimées par des formules de la logique temporelle arborescente CTL-X sont vérifiées sur ce graphe. Notre méthode de vérification présente des cas d'échec. Ce n'est pas surprenant car le problème est indécidable en général. Si aucun échec n'est rencontré, le graphe symbolique représente tous les états accessibles et les exécutions des pro­ grammes instanciés par un nombre de processus supérieur à une borne. L'algorithme de construction du graphe calcule cette borne. We propose a solution to solve part of the problem of the veri­ fication of properties of programs with a finite but unknown num­ ber of processes. We consider a subclass of parallel programs modeled with Petri nets. The originality of our method is to build a symbolic graph. The nodes of the graph are predicates that represent sets of states. Properties expressed in the branching temporal logic CTL-X are verified on this graph. Our verification method presents failure cases. This is not surpris­ ing because the problem is undecidable in the general case. If no failure cases are encountered, the symbolic graph represents all the reachable states and sequences of actions of programs instan­ tiated with a number of processes greater than a bound. The building algorithm computes this bound.