Nous nous intéressons dans cette thèse au model-checking des systèmes infinis, notamment<br />les systèmes paramétrés et les programmes récursifs parallèles. Nous présen\-tons un cadre<br />uniforme pour la vérification algorithmique de ces systèmes. Ce cadre est basé sur la <br />représentation des ensembles de configurations par des automates de mots ou d'arbres, et la<br />représentation des relations de transition des systèmes par des règles de réécritures de mots<br />ou de termes. Le problème de la vérification est ensuite réduit au calcul des ensembles des<br />accessibles dans ce cadre. Les contributions de cette thèse sont les suivantes:<br /><br />1- Définition d'une technique d'accélération générale. Nous proposons une méthode basée sur <br />des techniques d'extrapolation sur les automates, et nous étudions la puissance de cette approche.<br />2- Techniques de model-checking régulier pour la vérification des réseaux paramétrés avec des <br />topologies linéaires et arborescentes. En particulier, nous considérons les réseaux modélisés <br />par des systèmes de réécriture comprenant des semi-commutations, c-à-d. des règles de la forme ab -> ba,<br />et nous exhibons une classe de langages qui est effectivement fermée par ces systèmes.<br />3- Modélisation et vérification des programmes récursifs parallèles. Dans un premier temps, <br />nous étudions les modèles PRS qui sont plus généraux que les systèmes à pile, les réseaux de Petri,<br />et les systèmes PA; et nous proposons des algorithmes qui calculent les ensembles des accessibles <br />de (sous-classes de) PRS en considérant différentes sémantiques. <br /><br />Dans une autre approche, nous considérons des modèles basés sur des automates à pile communicants<br />et des systèmes de réécritures à-la CCS, et nous proposons des méthodes de vérification de ces modèles<br />basées sur le calcul d'abstractions des langages des chemins d'exécutions. Nous proposons un cadre<br />algébrique générique permettant le calcul de ces abstractions.