User: Guest  Login
Original title:
Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL 
Translated title:
Verifikation paralleler Programme mit den Methoden Owicki-Gries und Rely-Guarantee in Isabelle/HOL 
Year:
2002 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof. Ph.D.) 
Referee:
Nipkow, Tobias (Prof. Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr.) 
Format:
Text 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
parallel programs; verification; Owicki-Gries; Rely-Guarantee; garbage collection; Isabelle 
Translated keywords:
parallele Programme; Verifikation; Owicki-Gries; Rely-Guarantee; Müllsammlung; Isabelle 
Controlled terms:
Paralleles Programm; Verifikation; Isabelle ; HOL; Owicki-Gries-Methode; Rely-Guarantee-Methode 
TUM classification:
DAT 325d; DAT 706d 
Abstract:
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...    »
 
Translated abstract:
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 syst...    »
 
Publication :
Universitätsbibliothek der TU München 
Oral examination:
11.02.2002 
File size:
1005039 bytes 
Pages:
212 
Last change:
11.03.2010