Dozent: Dr. Dirk Nowotka

Vertiefungslinie: Sichere und zuverlässige Softwaresysteme

Zeit und Ort:
Vorlesung: Fr 11:30-13:00 im Raum V38.03 (Beginn: 28. April)
Übung: Mo 15:45-17:15 (14-tägig) im Raum 0.124
Übungstermine: 15.5., 29.5., 12.6., 26.6., 10.7., 24.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:

• Die alten Folien vom Sommersemester 2005 finden Sie hier.

Übungsblätter:

• Blatt 1 [PDF] (wird am 15.5. besprochen)
• Blatt 2 [PDF] (wird am 29.5. besprochen)
• Blatt 3 [PDF] (wird am 12.6. besprochen)
• Blatt 4 [PDF] (wird am 26.6. besprochen)
• Blatt 5 [PDF] (wird am 10.7. besprochen)
• Blatt 6 [PDF] (wird am 24.7. besprochen)

Skript:

• Stand vom 14.06.05 [PostScript] [PDF]

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.