  We address the problem of analyzing asynchronous event-driven programs, in
which concurrent agents communicate via unbounded message queues. The safety
verification problem for such programs is undecidable. We present in this paper
a technique that combines queue-bounded exploration with a convergence test: if
the sequence of certain abstractions of the reachable states, for increasing
queue bounds k, converges, we can prove any property of the program that is
preserved by the abstraction. If the abstract state space is finite,
convergence is guaranteed; the challenge is to catch the point k_max where it
happens. We further demonstrate how simple invariants formulated over the
concrete domain can be used to eliminate spurious abstract states, which
otherwise prevent the sequence from converging. We have implemented our
technique for the P programming language for event-driven programs. We show
experimentally that the sequence of abstractions often converges fully
automatically, in hard cases with minimal designer support in the form of
sequentially provable invariants, and that this happens for a value of k_max
small enough to allow the method to succeed in practice.
