Technical Report: DCC-2013-03

On the Mechanisation of Rely-Guarantee in Coq

Nelma Moreira, David Pereira

DCC\& Faculty of Science of University of Porto, Portugal,

Simão Melo de Sousa

LIACC, University of Beira Interior, Covilhã, Portugal,
January 2013


In this report we describe the formalisation of a simple imperative language with concurrent/parallel and atomic execution statements within the Coq theorem prover. Our formalisation includes the specification of a simple imperative programming language with statements for parallel and atomic execution of code, an underlying small-step structural semantics and a proof system that is sound with respect to such semantics. With this formalisation we give a first step towards the certified verification of shared- variable concurrent/parallel programs under the context of Cliff Jones? Rely-Guarantee reasoning and in the logic of Coq.