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

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

Artifact

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
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