Bild mit Unilogo
homeicon uni sucheicon suche siteicon sitemap kontakticon kontakt impressicon impressum
unilogo Universität Stuttgart 
Institut für Formale Methoden der Informatik

Abteilung Sichere und Zuverlässige Softwaresysteme

 

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)