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

TL;DRAbstract

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.

Chat with Paper

AI Agents for this Paper