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 presents a new challenge for program verification and hasresulted in the development of a variety of specialised logics. For C11-stylememory models, our previous work has shown that it is possible to extend Hoarelogic and Owicki-Gries reasoning to verify correctness of weak memory programs.The technique introduces a set of high-level assertions over C11 statestogether with a set of basic Hoare-style axioms over atomic weak memorystatements (e.g., reads/writes), but retains all other standard proofobligations for compound statements. This paper takes this line of work furtherby showing Nipkow and Nieto's encoding of Owicki-Gries in the Isabelle theoremprover can be extended to handle C11-style weak memory models in astraightforward manner. We exemplify our techniques over several litmus testsfrom the literature and a non-trivial example: Peterson's algorithm adapted forC11. For the examples we consider, the proof outlines can be automaticallydischarged using the existing Isabelle tactics developed by Nipkow and Nieto.The benefit here is that programs can be written using a familiar pseudocodesyntax with assertions embedded directly into the program.

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL