#### Owicki/Gries in Isabelle/HOL

#### Tobias Nipkow and Leonor Prensa Nieto

We present a formalization of the Gries/Owicki method for correctness
proofs of concurrent imperative programs with shared variables in the
theorem prover Isabelle/HOL. Syntax, semantics and proof rules are
defined in higher-order logic. The correctness of the proof rules
w.r.t. the semantics is proved. The verification of some typical
example programs like producer/consumer is presented.
dvi

ps

BibTeX:

@InProceedings{NipkowP-FASE99,
author = {Tobias Nipkow and Prensa Nieto, Leonor},
title = {{Owicki/Gries} in {Isabelle/HOL}},
booktitle = {Fundamental Approaches to Software Engineering (FASE'99)},
editor = {J.-P. Finance},
publisher = {Springer-Verlag},
series = {LNCS},
volume = 1577,
pages = {188--203},
year = 1999
}