ESOP 2003

The Rely-Guarantee Method in Isabelle/HOL

Leonor Prensa Nieto

We present the formalization of the rely-guarantee method in the theorem prover Isabelle/HOL. This method consists of a Hoare-like system of rules to verify concurrent imperative programs with shared variables in a compositional way. Syntax, semantics and proof rules are defined in higher-order logic. Soundness of the proof rules w.r.t.\ the semantics is proven mechanically. Also parameterized programs, where the number of parallel components is a parameter, are included in the programming language and thus can be verified directly in the system. We prove that the system is complete for parameterized programs. Finally, we show by an example how the formalization can be used for verifying concrete programs.

dvi

BibTeX:

@inproceedings{  Prensa-ESOP03,
author=          {Prensa Nieto, Leonor},
title=           {The {Rely-Guarantee} Method in {Isabelle/HOL}},
booktitle=       {European Symposium on Programming (ESOP'03)},
editor=          {P. Degano},
publisher=       Springer,
series=          {LNCS},
volume=          {2618},
pages=           {348--362},
year=            {2003}
}