Treffer: Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL ; Verifikation paralleler Programme mit den Methoden Owicki-Gries und Rely-Guarantee in Isabelle/HOL

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. ; In dieser Arbeit wird die Owicki-Gries Methode, und ihre kompositionelle Version, die Rely-Guarantee Methode, zur Verifikation paralleler imperativer Programme mit gemeinsamen Variablen zum ersten Mal in einem Theorembeweiser formalisiert. Syntax, Semantik und Beweisregeln werden in höherstufiger Logik definiert und die Korrektheit des Beweissystems bezüglich der Semantik wird bewiesen. Zahlreiche Beispiele, darunter parametrisierte parallele Programme, werden mit Hilfe einer Taktik für die systematische Generierung der Verifikations-Bedingungen verifiziert. Außerdem wird die Vollständigkeit der formalisierten Systeme für den Fall parametrisierter paralleler Programme bewiesen.