 |
Vorlesung Programmanalyse (SS 2004)
Dozentin:
Dr.
Barbara König
Vertiefungslinie: Sichere und zuverlässige Softwaresysteme
Zeit und Ort:
Di 11:30-13:00 im Raum 0.363
Hinweis: Die Vorlesung fällt am 8.6.04 aus!
Übung Do 14:00-15:30 (14-tägig) im Raum 0.453
Übungstermine: 29.4., 6.5., 27.5., 3.6., 24.6., 8.7., 22.7.
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 (bis zum 20.07.04):
Übungsblätter:
Skript:
Links:
- Java Bytecode Assembler jasmin
Literatur:
Neben der unten aufgeführten Literatur wird noch
das Skript vom Sommersemester 2003 überarbeitet
und bereitgestellt.
-
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)
-
David Schmidt:
-
Abstract interpretation and static analysis
International Winter School on Semantics and Applications
Montevideo, Uruguay, 21-31 July 2003
|
|
bk) |
© Universität Stuttgart |
Impressum