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 invocation and also unbounded nondeterminism. For this language a Hoare logic for both partial and total correctness is developed and on top of it a verification condition generator is implemented. The Hoare logic is designed to allow the integration of program analysis or software model checking into the verification. To demonstrate the continuity to a real programming language a subset of C is embedded into the verification environment. The whole work is developed in the theorem prover Isabelle. Therefore the correctness is machine-checked and in addition the rich infrastructure of the general purpose theorem prover Isabelle can be employed for the verification of imperative programs.     «

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...     »

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, partielle Applikation, dynamischer Methoden Aufruf und unbeschränkter Indeterminismus. Für dieses Sprachmodell wird eine Hoare Logik sowohl für partielle alsauch für totale Korrektheit entwickelt. Darauf aufbauend wird ein Verifikations-Bedingungs-Generator implementiert. Die Hoare Logik erlaubt die Integration von statischer Programmanalyse und Software Model Checkern in die Verifikation. Desweiteren wird eine Teilsprache von C in die Verifikationsumgebung eingebettet, um die Durchgängigkeit zu einer realen Programmiersprache zu demonstrieren. Die gesamte Entwicklung wurde im Theorembeweiser Isabelle durchgeführt. Dadurch wird zum einen die Korrektheit maschinell sichergestellt und zum anderen steht nun für die Verifikation von Programmen die reichhaltige Infrastruktur einer vollwertigen und universellen Beweisumgebung zur Verfügung.     «

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...     »