Introduction to Program Analysis (Proseminar)

Sommersemester 2021

News

  • 23.12.2020: Wir sind online!

Einführung und Themenvergabe

  • Slidecast zur Einführung (TBA)
  • Folien zur Einführung (TBA)
  • Foodle-Umfrage zur Themenvergabe (TBA)
  • Schulung in Literaturrecherche (TBA)

Termine

(TBA)Frist für Themenauswahl
(TBA)Letzte Rücktrittsmöglichkeit
(TBA)Vorlage der detaillierten Inhaltsübersicht
(TBA)Vollständige Fassung der Ausarbeitung
(TBA)Vollständige Fassung der Vortragsfolien
(TBA)Seminarvorträge

Beachten Sie, dass die vollständigen Fassungen von Ausarbeitung und Vortragsfolien Ihre finale Einreichung darstellen und sich von der endgültigen Version nur durch kleinere Anpassungen unterscheiden sollen, die nach Rücksprache mit der betreuenden Person erfolgen. Es ist aber möglich (und dringend empfohlen!), vor den jeweiligen Fristen Entwurfsversionen Ihrer Dokumente einzureichen.

Inhalt

Das Gebiet der Programmanalyse beschäftigt sich mit Methoden zur (automatischen) Analyse von Computersoftware. Die Anwendungen solcher Methoden sind sehr vielfältig und reichen von von der Unterstützung des Programmverständnisses über optimierende Compiler und Interpreter bis hin zum Nachweis von Korrektheitseigenschaften von Software. Entsprechend vielseitig sind auch die formalen Modelle, auf denen solche Analysen basieren, sowie die darauf operierenden Algorithmen. Das Ziel dieses Proseminars besteht darin, einen Überblick über grundlegende Modelle für Softwaresysteme, Logiken zur formalen Spezifikation ihrer Eigenschaften sowie Verfahren zur automatischen Überprüfung solcher Eigenschaften zu geben.

Themen

Nr.ThemaReferent(in)Betreuer(in)
Modelle
1Timed Automata
2Büchi Automata
3Markov Chains
4Probabilistic Automata
5(Dynamic) Fault Trees
Logiken
6Hoare Logic
7Linear Temporal Logic
8Computation Tree Logic
9Separation Logic
10Hennessy-Milner Logic
Statische Analyseverfahren
11Data-Flow Analysis
12Abstract Interpretation
13Type Systems
14Pointer Analysis
15Escape Analysis
16Shape Analysis
17Inductive Invariants
18Counterexample-Guided Abstraction Refinement (CEGAR)
Dynamische und Hybride Analyseverfahren
19Runtime Verification
20Bounded Model Checking
21Program Slicing

Anmeldung

Die Anmeldung erfolgt über eine zentrale Seite der Fachgruppe Informatik. Nachträgliche Anmeldungen sind nicht möglich.

Weitere Informationen

Kontakt

Thomas Noll