Nous considérons le problème de la vérification des réseaux paramétrés de processus, c'est-à-dire
des réseaux comprenant un nombre arbitraire de processus identiques. Nous modélisons ces systèmes
par des systèmes de réécriture définissant des relations régulières et nous représentons les 
ensembles de configurations par des langages réguliers. Nous réduisons le problème de  la 
vérification à celui du calcul de R^*(L), où R (resp. L), une relation régulière (resp. un langage
régulier). Nous proposons alors deux résultats principaux:

1- Nous montrons  qu'une classe de réguliers (SRE^+), qui correspond aux langages de niveau 3/2 de
la hiérarchie de Straubing, est effectivement fermée par permutations: nous proposons un algorithme
qui calcule R^*(L), pour tout langage  L de la classe et tout ensemble de permutations  R.
2- Nous définissons  une approche symbolique pour le calcul de R^*(L) basée sur une technique  automatique 
d'extrapolation qui permet d'accélérer les calculs de points fixes pour aider la convergence.  Nous 
avons réalisé un prototype d'outil basé sur cette technique d'extrapolation. Cet outil a permis de vérifier 
automatiquement et efficacement les protocoles d'exclusion mutuelle de Dijkstra,  de Burns, de Szymanski,
de celui de Lamport connu sous le nom du ``Bakery algorithm'' et le  ``token passing protocol''.