Benutzer: Gast  Login
Originaltitel:
Verification of Sequential Imperative Programs in Isabelle/HOL 
Übersetzter Titel:
Verifikation von sequentiellen imperativen Programmen in Isabelle/HOL 
Jahr:
2006 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof. Ph.D.); Paul, Wolfgang J. (Prof. Dr.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Hoare-Logic; Verification; Theorem Proving; Semantics 
Übersetzte Stichworte:
Hoare-Logik; Verifikation; Theorembeweisen; Semantik 
Schlagworte (SWD):
Automatisches Beweisverfahren; Hoare-Logik 
TU-Systematik:
DAT 325d; DAT 706d 
Kurzfassung:
The purpose of this thesis is to create a verification environment for sequential imperative programs. First a general language model is proposed, which is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method inv...    »
 
Übersetzte Kurzfassung:
Ziel der Dissertation ist es, eine Verifikationsumgebung für sequentielle imperative Programme zu schaffen. Zunächst wird unabhängig von einer konkreten Programmiersprache ein allgemeines Sprachmodell entwickelt, das ausdrucksstark genug ist um alle gängigen Programmiersprachkonzepte abzudecken: Gegenseitig rekursive Prozeduren, abrupte Terminierung und Ausnahmebehandlung, Laufzeitfehler, lokale und globale Variablen, Zeiger und Halde, Ausdrücke mit Seiteneffekten, Zeiger auf Prozeduren, partiel...    »
 
Veröffentlichung:
Universitätsbibliothek der Technischen Universität München 
Mündliche Prüfung:
09.05.2006 
Dateigröße:
1504765 bytes 
Seiten:
263 
Letzte Änderung:
10.07.2007