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

Weak memory models specify the semantics of concurrent programs on multi-corearchitectures. Reasoning techniques for weak memory models are oftenspecialized to one fixed model and verification results are hence nottransferable to other memory models. A recent proposal of a genericverification technique based on axioms on program behaviour expressed viaweakest preconditions aims at overcoming this specialization to dedicatedmodels. Due to the usage of weakest preconditions, reasoning however takesplace on a very low level requiring the application of numerous axioms forderiving program properties, even for a single statement. In this paper, welift reasoning in this generic verification approach to a more abstract level.Based on a view-based assertion language, we provide a number of novel proofrules for directly reasoning on the level of program constructs. We provesoundness of our proof rules and exemplify them on the write-to-read causality(WRC) litmus test. A comparison to the axiom-based low-level proof reveals asignificant reduction in the number of required proof steps.

Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version)