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

ps

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