English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We address the problem of analyzing asynchronous event-driven programs, inwhich concurrent agents communicate via unbounded message queues. The safetyverification problem for such programs is undecidable. We present in this papera technique that combines queue-bounded exploration with a convergence test: ifthe sequence of certain abstractions of the reachable states, for increasingqueue bounds k, converges, we can prove any property of the program that ispreserved by the abstraction. If the abstract state space is finite,convergence is guaranteed; the challenge is to catch the point k_max where ithappens. We further demonstrate how simple invariants formulated over theconcrete domain can be used to eliminate spurious abstract states, whichotherwise prevent the sequence from converging. We have implemented ourtechnique for the P programming language for event-driven programs. We showexperimentally that the sequence of abstractions often converges fullyautomatically, in hard cases with minimal designer support in the form ofsequentially provable invariants, and that this happens for a value of k_maxsmall enough to allow the method to succeed in practice.

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)