13 DEZEMBRO / QUARTA FEIRA / 11:00
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

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,
e-mail: nam@dcc.fc.up.pt, dpereira@liacc.up.pt

Simão Melo de Sousa

LIACC, University of Beira Interior, Covilhã, Portugal,
e-mail:desousa@ubi.pt
January 2013

Abstract

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.


FCUP 2017