This paper presents a new contribution to the model-checking of multithreaded programs with 
recursive  procedure calls, result passing between recursive procedures, dynamic creation of parallel processes, and synchronisation between parallel
threads. To represent  such programs  accurately, we define the model  SPAD that can be seen as the extension  with synchronisation
of the class PAD (the subclass of the rewrite systems PRS where  parallel composition is not allowed in the left-hand sides of the rules).
We consider in this paper  the reachability problem of this model, which is undecidable.
As in  [BET03,BET04], we reduce this problem to the computation of abstractions of the sets of execution paths of the program, and 
we propose a generic technique that can compute different abstractions (of different 
precisions and different costs) of these sets.