inf481 - Software Analysis (Vollständige Modulbeschreibung)

Softwareanalysen dienen der Berechnung von Fakten über Programme aus dem Programmtext. Solche Fakten können beispielsweise vom Compiler zur Optimierung während der Übersetzung eingesetzt werden, aber auch zur Verifikation von Korrektheitseigenschaften genutzt werden. Die Studierenden lernen verschiedene Analyseverfahren kennen, spezifizieren selber solche Verfahren und implementieren sie.
Fachkompetenzen
Die Studierenden:

• lernen Datenflussanalysen kennen und können selber solche spezifizieren
• benenen die Bestandteile eines Datenflusssystems
•  wissen, wann Widening Operatoren für eine Datenflussanalyse nötig sind
• können abstrakte Domänen und Operatoren für die Abstrakte Interpretation entwickeln und anwenden
• kennen Prädikatabstraktion und das Prinzip der Gegenbeispiel-gesteuerten Abstraktionsverfeinerung
• wissen, wann und wozu SSA Formen eingesetzt werden
• können die Präzision und Skalierbarkeit von points-to Analysen abschätzen

Methodenkompetenzen

• können Analysen formal definieren
• können Eigenschaften von Analysen beweisen
• können Analysen implementieren

Sozialkompetenzen
Die Studierenden:

• bearbeiten in Gruppen Übungsaufgaben, diskutieren Ergebnisse
• implementierten verteilt an einer Aufgabenstellung

Selbstkompetenzen
Die Studierenden:

• organisieren sich selber bei der Arbeit an den Aufgabenstellungen des Moduls

• Datenflussanalysen
• Abstrakte Interpretation
• Prädikatabstraktion, CEGAR
• SSA-Formen
• Slicing
• Points-to Analysen
• Symbolische Ausführung

• Nielson, Nielson, Hankin: Principles of Program Analysis, Springer, 2004.

am Ende des Semesters

Klausur oder mündl. Prüfung