Benutzer: Gast  Login
Originaltitel:
Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL 
Übersetzter Titel:
Verifikation paralleler Programme mit den Methoden Owicki-Gries und Rely-Guarantee in Isabelle/HOL 
Jahr:
2002 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof. Ph.D.); Esparza Estaun, Francisco Javier (Prof. Dr.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
parallel programs; verification; Owicki-Gries; Rely-Guarantee; garbage collection; Isabelle 
Übersetzte Stichworte:
parallele Programme; Verifikation; Owicki-Gries; Rely-Guarantee; Müllsammlung; Isabelle 
Schlagworte (SWD):
Paralleles Programm; Verifikation; Isabelle ; HOL; Owicki-Gries-Methode; Rely-Guarantee-Methode 
TU-Systematik:
DAT 325d; DAT 706d 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
11.02.2002 
Dateigröße:
1005039 bytes 
Seiten:
212 
Letzte Änderung:
11.03.2010