Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers

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 convergen... View More