 |
Vorlesung Programmanalyse (SS 2003)
Dozentin:
Dr.
Barbara König
Vertiefungslinie: Theoretische Informatik
Zeit und Ort:
Mo 11:30-13:00 im Raum 0.118
Übung Do 14:00-15:30 (14-tägig) im Raum 0.453
Übungstermine: 8. Mai, 22. Mai, 5. Juni, 26. Juni, 3. Juli,
17. Juli, 24. Juli
Hörerkreis:
Studierende im Hauptstudium
Empfehlenswert für:
Erweiterte Kenntnisse in den Gebieten Verifikation, Programmanalyse,
Semantik
Inhalt:
Zur automatischen Verifikation und Validierung von Programmen und
Systemen benötigt man Verfahren, die bei Eingabe eines Programms
und einer zugehörigen Spezifikation entscheiden, ob das Programm
diese Spezifikation erfüllt. Im allgemeinen ist dieses Problem
unentscheidbar, es gibt jedoch viele sicherheitskritische Programme,
die man dennoch gerne maschinell analysieren und verifizieren
möchte. Auch sie können analysiert werden, wenn man
nicht-vollständige Verfahren zuläßt. Man verlangt,
dass diese Analyseverfahren niemals ein fehlerhaftes Programm als
korrekt ansehen, es ist aber zulässig, korrekte Programme
abzulehnen (einseitiger Irrtum). Auf diese Weise kann immer noch eine
große Menge von Programmen analysisert und ihre Korrektheit
verifiziert werden. Ein anderer wichtiger Anwendungsbereich ist die
Programmoptimierung im Compilerbau.
In der Vorlesung werden grundlegende Verfahren zur Programmanalyse,
wie Datenflußanalyse, Abstrakte Interpretation und Typsysteme
vorgestellt und ihre Anwendung verdeutlicht.
In den letzten Jahren gab es auf diesem Gebiet eine rege
Forschungstätigkeit. Daher wird sich ein Teil der Vorlesung mit
neueren Ergebnissen, vor allem aus dem Bereich der Analyse
nebenläufiger Systeme beschäftigen. Darunter fallen die
Anwendung von Abstract Interpretation auf reaktive Systeme und
Typsysteme für Prozeßkalküle mit Mobilität
(pi-Kalkül). Außerdem wird der Java Bytecode Verifier als
Anwendungsbeispiel von Datenflußanalyse vorgestellt.
Folien:
Mit psnup -l -4 <infile> <outfile> bringt man
vier Seiten PostScript-Datei auf einer Seite unter und
kann so praktischer drucken.
Skript: Das Skript zur Vorlesung wird
inkrementell erstellt. Bereits fertige Kapitel können
hier heruntergeladen werden. Das aktuelle Skript enthält:
- Einleitung (Kapitel 1)
- Notation (Kapitel 2)
- Datenflußanalyse (Kapitel 3)
- Java Bytecode Verifier (Kapitel 4)
- Grundlagen der abstrakten Interpretation (Kapitel 5)
(Die Abschnitte 5.2.3 und 5.2.4 gehören nicht mehr
zum in der Vorlesung behandelten Stoff)
- WHILE-Programme (Anhang A)
- Ordnungen und Fixpunkte (Anhang B)
- Literaturverzeichnis
Kommentare und Fehlermeldungen bitte per E-Mail an koenigba@informatik.uni-stuttgart.de
Übungsblätter:
Literatur:
-
Flemming Nielson, Hanne Riis Nielson,
Chris Hankin:
-
Principles of Program Analysis
Springer-Verlag, Berlin - Heidelberg - New York, 1999
(Datenflußanalyse, Abstrakte Interpretation,
While-Programme und Fixpunkttheorie)
(Das Buch steht im Semesterapparat der Bibliothek.)
-
Neil D. Jones, Flemming Nielson:
-
Abstract interpretation: a semantics-based tool for
program analysis
in
S. Abramsky, Dov M. Gabbay, T.S.E.
Maibaum:
Handbook of Logic in Computer Science, Volume 4:
Semantic Modelling
Clarendon Press, Oxford, 1995
(Abstrakte Interpretation)
-
John C. Mitchell:
-
Foundations for Programming Languages
MIT Press, 1996
(Typsysteme)
|
|
bk) |
© Universität Stuttgart |
Impressum