TIKI Home INFORMATIK VII

Theoretische Informatik und
Grundlagen der Künstlichen Intelligenz

Informatik TUM

Verfahren zur Programmanalyse (WS 2002/03)


Verfahren zur Programmanalyse (WS 2002/03)


Dozentin:
Dr. Barbara König

Bereich:
3 SWS Vorlesung im Bereich Informatik III (Theoretische Informatik)
Vertiefende Vorlesung im Gebiet Semantik und Logik.

Zeit und Ort (Achtung: Raumänderung!):
Mi 10:00-12:00 im Raum 03.11.018, Fr 13:00-14:00 im Raum 03.07.023

Hörerkreis:
Studierende im Hauptstudium der Informatik
Studierende mit Nebenfach Informatik

Voraussetzungen:
Stoff des Informatik Grundstudiums

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 effiziente Verfahren für endliche oder eingeschränkte Systeme.

Allerdings gibt es viele sicherheitskritische Programme, die diese Einschränkungen nicht erfüllen. 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, Typsysteme und Abstract Interpretation 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 Typsysteme für Prozeßkalküle mit Mobilität (pi-Kalkül) und die Anwendung von Abstract Interpretation auf reaktive Systeme. 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: Kommentare und Fehlermeldungen bitte per E-Mail an koenigb@in.tum.de

Demo:

Typsystem von ML (mit Programmbeispielen)

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)

John C. Mitchell:
Foundations for Programming Languages
MIT Press, 1996
(Typsysteme)

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)


Barbara König
Last modified: Tue Feb 11 09:09:00 MET 2003