Introduction to Program Analysis

Proseminar, Sommersemester 2020

News

  • 24.03.2020: Das Proseminar wird bis auf weiteres ohne Präsenzveranstaltungen in elektronischer Form organisiert. Das erste Material wird spätestens am 14. April zugänglich gemacht.
  • 20.01.2020: Wir sind online!

Einführung und Themenvergabe

Termine

17.04.2020Frist für Themenauswahl
11.05.2020Letzte Rücktrittsmöglichkeit
18.05.2020Vorlage der detaillierten Inhaltsübersicht
08.06.2020Vollständige Fassung der Ausarbeitung
06.07.2020Vollständige Fassung der Vortragsfolien
15./16.07.2020 (?)Blockseminar im Seminarraum Informatik 2 (Gebäude E1, Raum 4201b

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 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 AutomataAdrian Holt, Florian SprünkenThomas Noll
2Büchi AutomataMatthis Franzgrote, Eren YalcinIra Fesefeldt
3Markov ChainsGeorg Albrecht, Felix WöhnerJip Spel
4Probabilistic AutomataJennifer Sue Berendt, Tabea HegewaldtJip Spel
5(Dynamic) Fault TreesJannis Feldmann, Jordan RosensteinThomas Noll
Logiken
6Hoare LogicLeon Barth, Haiyan SaadiLutz Klinkenberg
7Linear Temporal LogicBenjamin Faust, Amelie RathTobias Winkler
8Computation Tree LogicGiang Lai, Antoine OrigerTobias Winkler
9Separation Logic
10Hennessy-Milner Logic
Statische Analyseverfahren
11Data-Flow AnalysisJoshua Noah Feld, Youssef KharitaKevin Batz
12Abstract Interpretation
13Type SystemsChristian Andreas Heuer, Dominik NguyenIra Fesefeldt
14Pointer AnalysisAmelie DIttmann, Gian Luca SpitzerPhilipp Berger
15Escape Analysis
16Shape Analysis
17Inductive InvariantsAnike Heikrodt, Niklas MolczanskiKevin Batz
18Counterexample-Guided Abstraction Refinement (CEGAR)
Dynamische und Hybride Analyseverfahren
19Runtime VerificationLeila Mkadmi, Hannes PieperPhilipp Berger
20Bounded Model Checking
21Program SlicingMohamed-Wassim Deghdagh, Alexander FerberLutz Klinkenberg

Anmeldung

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

Weitere Informationen

Kontakt

Thomas Noll