Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25913
Titel: Verification of the C0 compiler implementation on the source code level
Verfasser: Petrova, Elena
Sprache: Englisch
Erscheinungsjahr: 2007
SWD-Schlagwörter: Programmverifikation
Compiler
Implementierung
Hoare-Logik
Softwarespezifikation
Freie Schlagwörter: program verification
C0
compiler implementation
Hoare Logic
specification
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: This thesis concerns practical application of two methods for program verification. The programming language we consider is a C dialect, called C0, which supports dynamic memory allocation, recursion, pointer types, etc. First, we verify a program using a formalization of small-step semantics of C0. The example we study is a small loop program, which allocates a linked list of the given length on the heap. Second, we describe the verification of a compiler implementation in a Hoare Logic in the sense of partial correctness. The source and implementation language of the compiler is C0. The correctness statement is divided into independent parts: i) the correctness of the compilation algorithm with respect to the target machine and ii) the correctness of the implementation with respect to the specified algorithm. This thesis considers the second task. We give the formal specification of the compilation algorithm and develop the connection of the implementation data structures to the abstract types used in the specification. Finally, we show the correctness of the compiler implementation with respect to the specification.
Die vorliegende Arbeit befasst sich mit der praktischen Anwendung von zwei Methoden zur Programmverifikation. Die Programmiersprache, die dabei betrachtet wird, ist C0, ein C Dialekt, der unter anderem dynamische Allokation von Speicher, Rekursion und Pointer unterstützt. Zuerst beweisen wir die Korrektheit eines Programms mit Hilfe der formalen Small-Step Semantik von C0. Das Beispiel, das wir untersuchen, ist ein kleines Programm, das in einer Schleife eine gelinkte Liste gegebener Länge auf dem Heap alloziert. Danach beschreiben wir die Verifikation einer Compiler-Implementierung mittels einer Hoare Logik für partielle Korrektheit. Die Quell- und Implementierungssprache des Compilers ist C0. Die Korrektheitsaussage ist in unabhängige Aufgaben aufgeteilt: i) die Korrektheit des Compileralgorithmus bezüglich der Zielarchitektur und ii) die Korrektheit der Implementierung bezüglich dieses Algorithmus. Die vorliegende Arbeit beschäftigt sich mit der zweiten Aufgabe. Wir beschreiben die formale Spezifikation des Compileralgorithmus und entwickeln eine Verbindung zwischen den Datenstrukturen der Implementierung und den abstrakten Typen, die in der Spezifikation benutzt werden. Schließlich zeigen wir die Korrektheit der Compilerimplementierung bezüglich der Spezifikation.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-14011
hdl:20.500.11880/25969
http://dx.doi.org/10.22028/D291-25913
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 4-Mai-2007
SciDok-Publikation: 21-Dez-2007
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Dissertation_2325_Petr_Elen_2007.pdf1,13 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.