Owicki-Gries Reasoning for C11 RAR (Artifact)

Authors Sadegh Dalvandi , Simon Doherty , Brijesh Dongol , Heike Wehrheim

Thumbnail PDF

Artifact Description

  • Filesize: 333 kB
  • 2 pages

Document Identifiers

Author Details

Sadegh Dalvandi
  • University of Surrey, United Kingdom
Simon Doherty
  • University of Sheffield, United Kingdom
Brijesh Dongol
  • University of Surrey, United Kingdom
Heike Wehrheim
  • Paderborn University, Germany

Cite AsGet BibTex

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)



The paper "Owicki-Gries Reasoning for C11 RAR" introduces a new proof calculus for the C11 RAR memory model that allows Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. The proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. The artifact includes the Isabelle formalisation of the proof method introduced in the paper. It also contains the formalisation and proof of all case studies presented in the paper. All of the theorems are accompanied with their respective proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Hoare logic
  • Theory of computation → Concurrency
  • Theory of computation → Operational semantics
  • Theory of computation → Program reasoning
  • C11
  • Verification
  • Hoare logic
  • Owicki-Gries
  • Isabelle


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads