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

Canonical abstraction is a static analysis technique that represents statesas 3-valued logical structures, and produces finite abstract systems. Despiteproviding a finite bound, these abstractions may still suffer from the stateexplosion problem. Notably, for concurrent programs with arbitraryinterleaving, if threads in a state are abstracted based on their location,then the number of locations will be a combinatorial factor in the size of thestatespace. We present an approach using canonical abstraction that avoids thisstate explosion by "collapsing" all of the threads in a state into a singleabstract representative. Properties of threads that would be lost by theabstraction, but are needed for verification, are retained by definingconditional "soft invariant" instrumentation predicates. This technique is usedto adapt previous models for verifying linearizability of nonblockingconcurrent data structure algorithms, resulting in exponentially smallerstatespaces.

Collapsing Threads Safely with Soft Invariants