FASE 99

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

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
}