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.
ps
BibTeX:
@article{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,series=LNCS,volume=1577,
pages={188--203},year=1999}