PhD Thesis

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}}
}