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.



@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,