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

Deductive verification techniques for C11 programs have advancedsignificantly in recent years with the development of operational semantics andassociated logics for increasingly large fragments of C11. However, thesesemantics and logics have been developed in a restricted setting to avoid thethin-air-read problem. In this paper, we propose an operational semantics thatleverages an intra-thread partial order (called semantic dependencies) inducedby a recently developed denotational event-structure-based semantics. We provethat our operational semantics is sound and complete with respect to thedenotational semantics. We present an associated logic that generalises arecent Owicki-Gries framework for RC11 (repaired C11), and demonstrate the useof this logic over several example proofs.

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)