Document Open Access Logo

Owicki-Gries Reasoning for C11 RAR (Artifact)

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

PDF
Thumbnail PDF

Artifact Description

DARTS.6.2.15.pdf
  • 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

Funding

  • Dalvandi, Sadegh: Supported by EPSRC Grant EP/R032556/1.
  • Doherty, Simon: Supported by EPSRC Grant EP/R032351/1.
  • Dongol, Brijesh: Supported by EPSRC Grant EP/R032556/1.
  • Wehrheim, Heike: Supported by DFG grant WE 2290/12-1.

Cite As Get 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) https://doi.org/10.4230/DARTS.6.2.15

Artifact

  MD5 Sum: 2af93230c931e280e342352f5c7ce83e (Get MD5 Sum)

Abstract

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
Keywords
  • C11
  • Verification
  • Hoare logic
  • Owicki-Gries
  • Isabelle

Metrics

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

Related Article

  • Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim, "Owicki-Gries Reasoning for C11 RAR", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 11:1 - 11:26, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.11
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact