User: Guest  Login
Original title:
Verification of Sequential Imperative Programs in Isabelle/HOL 
Translated title:
Verifikation von sequentiellen imperativen Programmen in Isabelle/HOL 
Year:
2006 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof. Ph.D.) 
Referee:
Nipkow, Tobias (Prof. Ph.D.); Paul, Wolfgang J. (Prof. Dr.) 
Format:
Text 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Hoare-Logic; Verification; Theorem Proving; Semantics 
Translated keywords:
Hoare-Logik; Verifikation; Theorembeweisen; Semantik 
Controlled terms:
Automatisches Beweisverfahren; Hoare-Logik 
TUM classification:
DAT 325d; DAT 706d 
Abstract:
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...    »
 
Translated abstract:
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...    »
 
Publication :
Universitätsbibliothek der Technischen Universität München 
Oral examination:
09.05.2006 
File size:
1504765 bytes 
Pages:
263 
Last change:
10.07.2007