1: \begin{abstract}

2:   We address the problem of analyzing asynchronous event-driven programs,

3:   in which concurrent agents communicate via un\-bound\-ed message

4:   queues. The safety verification problem for such programs is

5:   undecidable. We present in this paper a technique that

6:   combines \emph{queue-bounded exploration} with a \emph{convergence test}:

7:   if the sequence of certain abstractions of the reachable states, for

8:   increasing queue bounds $k$, converges, we can prove any property of the

9:   program that is preserved by the abstraction. If the abstract state space

10:   is finite, convergence is \emph{guaranteed}; the challenge is to catch

11:   the point $\convergencePoint$ where it happens. We further demonstrate

12:   how simple invariants formulated over the \emph{concrete} domain can be

13:   used to eliminate spurious \emph{abstract} states, which otherwise

14:   prevent the sequence from converging. We have implemented our technique

15:   for the \pfeature P programming language for event-driven programs. We

16:   show experimentally that the sequence of abstractions often converges

17:   fully automatically, in hard cases with minimal designer support in the

18:   form of sequentially provable invariants, and that this happens for a

19:   value of $\convergencePoint$ small enough to allow the method to succeed

20:   in practice.

21: \end{abstract}

22: