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

Solidity smart contracts are programs that manage up to 2^160 users on ablockchain. Verifying a smart contract relative to all users is intractable dueto state explosion. Existing solutions either restrict the number of users tounder-approximate behaviour, or rely on manual proofs. In this paper, wepresent local bundles that reduce contracts with arbitrarily many users tosequential programs with a few representative users. Each representative userabstracts concrete users that are locally symmetric to each other relative tothe contract and the property. Our abstraction is semi-automated. Therepresentatives depend on communication patterns, and are computed via staticanalysis. A summary for the behaviour of each representative is providedmanually, but a default summary is often sufficient. Once obtained, a localbundle is amenable to sequential static analysis. We show that local bundlesare relatively complete for parameterized safety verification, under moderateassumptions. We implement local bundle abstraction in SmartACE, and showorder-of-magnitude speedups compared to a state-of-the-art verifier.

Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)