License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.6.2.15
URN: urn:nbn:de:0030-drops-132123
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13212/
Go back to Dagstuhl Artifacts Series

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

Owicki-Gries Reasoning for C11 RAR (Artifact)

pdf-format:
DARTS-6-2-15.pdf (0.3 MB)

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.

BibTeX - Entry

@Article{dalvandi_et_al:DARTS:2020:13212,
  author =	{Sadegh Dalvandi and Simon Doherty and Brijesh Dongol and Heike Wehrheim},
  title =	{{Owicki-Gries Reasoning for C11 RAR (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13212},
  URN =		{urn:nbn:de:0030-drops-132123},
  doi =		{10.4230/DARTS.6.2.15},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}

Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle
Collection: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Related Scholarly Article: https://doi.org/10.4230/LIPIcs.ECOOP.2020.11
Issue Date: 2020
Date of publication: 06.11.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI