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 present an approach to parameterized reachability for communicatingfinite-state threads that formulates the analysis as a satisfiability problem.In addition to the unbounded number of threads, the main challenge forSAT/SMT-based reachability methods is the existence of unbounded loops in theprogram executed by a thread. We show in this paper how simple loops can beaccelerated without approximation into Presburger arithmetic constraints. Theconstraints are obtained via symbolic execution and are satisfiable exactly ifthe given program state is reachable. We summarize loops nested inside otherloops using recurrence relations derived from the inner loop's acceleration.This summary abstracts the loop iteration parameter and may thusoverapproximate. An advantage of our symbolic approach is that the process ofbuilding the Presburger formulas may instantly reveal their unsatisfiability,before any arithmetic has been performed. We demonstrate the power of thistechnique for proving and refuting safety properties of unbounded-threadprograms and other infinite-state transition systems.

Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report)