We consider in this thesis the  model-checking problem of infinite state systems, 
namely parametrized systems and recursive multithreaded programs. We present a 
uniform framework for the algorithmic verification  of these systems. This framework
is based on the  representation  of sets of configurations using word/tree automata,
and the representation  of the transition relations of the systems using word/tree 
rewriting rules. The verification problem is then reduced to the computation of the
reachability sets in this  framework. The contributions of this thesis are the following:

1-  Definition of a general  acceleration technique. We propose  a method based on   
extrapolation techniques on  automata, and we study the power of this approach.
2-  Regular  model-checking techniques for the  verification of   parametrized  
networks with linear and tree-like  topologies. In  particular, we  consider the 
networks modeled by rewriting systems containing   semi-commutations, i.e.. rules of 
the  form  ab -> ba, and we isolate a  class  of  languages which is effectively closed
under these systems.
3- Modeling and  verification of  recursive multithreaded programs.  We study first the 
models  PRS which are more general than pushdown systems, Petri nets, and PA systems; 
and we propose algorithms that compute the reachability sets of (subclasses of) PRS  when
considering different semantics. 

In another approach, we consider models based on communicating pushdown systems and CCS-like
rewriting systems; and we propose  verification methods of these models based on the computation
of abstractions of execution path languages. We propsoe a generic  algebraic  framework that 
allows the computation of these abstractions.  

Key words.  Regular model-checking, verification, rewriting systems, automata, parametrized
systems, verification of recursive multithreaded programs, PRS, reachability analysis, acceleration.