 |
Vorlesung
"Automatische Analyse und Verifikation von Programmen"
(SS 2005)
Dozentin:
Dr.
Barbara König
Vertiefungslinie: Sichere und zuverlässige Softwaresysteme
Zeit und Ort:
Di 11:30-13:00 im Raum 0.108 (Beginn: 12. April)
Übung Do 14:00-15:30 (14-tägig) im Raum 0.108
Übungstermine: 21.4., 28.4., 12.5., 2.6., 16.6., 7.7.
Hörerkreis:
Studierende im Hauptstudium
Empfehlenswert für:
Erweiterte Kenntnisse in den Gebieten Verifikation, Programmanalyse,
Semantik
Bemerkung:
Diese Vorlesung hieß früher "Programmanalyse".
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:
- Endgültiger Stand der Folien
[PDF]
Übungsblätter:
Skript:
Links:
- wAnalyzer - Ein Tool für die Datenflussanalyse
- PAG/WWW - Experiencing Program Analysis
- Java Bytecode Assembler jasmin
- PPL: The Parma Polyhedra Library
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)
-
David Schmidt:
-
Abstract interpretation and static analysis
International Winter School on Semantics and Applications
Montevideo, Uruguay, 21-31 July 2003
-
Tobias Nipkow:
-
Verified bytecode verifiers.
In Proc. of FOSSACS '01, pages 347--363. Springer-Verlag, 2001.
LNCS 2030.
-
Patrick Cousot, Nicolas Halbwachs:
-
Automatic discovery of linear restraints among variables
of a program.
In Proc. of POPL '78 (Tucson, Arizona), pages 84--96. ACM,
1978.
-
Robin Milner:
-
The polyadic pi-calculus: a tutorial.
Tech. Rep. ECS-LFCS-91-180, University of Edinburgh,
Laboratory for Foundations of Computer Science, 1991.
|
|
bk) |
© Universität Stuttgart |
Impressum