User: Guest  Login
Original title:
Verification of Sequential Imperative Programs in Isabelle/HOL
Translated title:
Verifikation von sequentiellen imperativen Programmen in Isabelle/HOL
Author:
Schirmer, Norbert
Year:
2006
Document type:
Dissertation
Faculty/School:
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
WWW:
https://mediatum.ub.tum.de/?id=601799
Date of submission:
31.10.2005
Oral examination:
09.05.2006
File size:
1504765 bytes
Pages:
263
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss20060529-1116038779
Last change:
10.07.2007
 BibTeX