Nous nous intéressons dans cette thèse au model-checking  des systèmes infinis, notamment
les systèmes paramétrés et les  programmes récursifs parallèles. Nous présen\-tons un cadre
uniforme pour la vérification algorithmique de ces systèmes. Ce cadre est basé sur la 
représentation des ensembles de configurations par des automates de mots ou d'arbres, et la
représentation des relations de transition des systèmes  par des règles de réécritures de mots
ou de termes.  Le problème de la vérification est ensuite réduit au calcul  des ensembles des
accessibles dans ce cadre. Les contributions de cette thèse sont les suivantes:

1- Définition d'une technique d'accélération générale. Nous proposons  une méthode basée sur 
des  techniques d'extrapolation sur les  automates, et nous étudions la puissance  de cette approche.
2- Techniques de model-checking régulier pour la vérification des réseaux  paramétrés avec des 
topologies linéaires et arborescentes. En particulier, nous considérons  les réseaux modélisés 
par des systèmes de réécriture comprenant des semi-commutations, c-à-d. des règles de la forme ab -> ba,
et nous exhibons une classe de langages qui est  effectivement fermée par ces systèmes.
3- Modélisation et vérification des programmes récursifs parallèles. Dans un premier temps, 
nous étudions les modèles PRS qui sont  plus généraux que les systèmes à pile, les réseaux de Petri,
et les systèmes PA; et nous   proposons des algorithmes  qui calculent les ensembles des accessibles 
de (sous-classes de) PRS en considérant  différentes sémantiques. 

Dans une autre approche, nous considérons des modèles basés sur des automates à pile communicants
et des systèmes de réécritures à-la CCS, et nous proposons des méthodes de vérification de ces modèles
basées sur le calcul d'abstractions des langages des chemins  d'exécutions. Nous proposons un cadre
algébrique générique permettant le calcul de ces abstractions.

Mots clés: Regular model-checking, vérification, systèmes de réécriture, automates, systèmes paramétrés,
vérification de  programmes récursifs parallèles, PRS, analyse d'acessibilité, accélération.