  We address the problem of verifying message passing programs, defined as a
set of parallel processes communicating through unbounded FIFO buffers. We
introduce a bounded analysis that explores a special type of computations,
called k-synchronous. These computations can be viewed as (unbounded) sequences
of interaction phases, each phase allowing at most k send actions (by different
processes), followed by a sequence of receives corresponding to sends in the
same phase. We give a procedure for deciding k-synchronizability of a program,
i.e., whether every computation is equivalent (has the same happens-before
relation) to one of its k-synchronous computations. We also show that
reachability over k-synchronous computations and checking k-synchronizability
are both PSPACE-complete. Furthermore, we introduce a class of programs called
{\em flow-bounded} for which the problem of deciding whether there exists a k>0
for which the program is k-synchronizable, is decidable.
