#### Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL.

#### Leonor Prensa Nieto

This thesis presents the first formalization of the Owicki-Gries
method and its compositional version, the rely-guarantee method, in
a theorem prover. These methods are widely used for correctness
proofs of parallel imperative programs with shared variables. We
define syntax, semantics and proof rules in Isabelle/HOL, which is
the instantiation of higher-order logic in the theorem prover
Isabelle. The proof rules also provide for programs parameterized in
the number of parallel components. Their correctness w.r.t. the
semantics is proven mechanically and the completeness proofs for
both methods are extended to the new case of parameterized programs.
For the automatic generation of verification conditions we define a
tactic based on the proof rules. Using this tactic we verify several
non-trivial examples for parameterized and non-parameterized
programs.
pdf

Slides(in german)

BibTeX:

@PhdThesis{Prensa-PhD,
author = {Leonor Prensa Nieto},
title = {Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL},
school = {Technische Universit{\"a}t M{\"u}nchen},
year = {2002},
note = {Available at \url{http://tumb1.biblio.tu-muenchen.de/publ/diss/allgemein.html}}
}