Introduction to Program Analysis

Proseminar, Sommersemester 2019

News

  • 10.01.2019: Wir sind online!

Termine

03.04.2019, 15:00 Einführungsveranstaltung im Seminarraum 5052 (Informatikzentrum)
24.04.2019 Letzte Rücktrittsmöglichkeit
02.06.2019 Vorlage der detaillierten Inhaltsübersicht
Di, 30.04., 10:00
Do, 02.05., 15:00
Fr, 03.05., 10:00
Di, 14.05., 15:00
Einführung in die Literaturrecherche (Informatik-Bibliothek)
23.06.2019 Vollständige Fassung der Ausarbeitung
07.07.2019 Vollständige Fassung der Folien
15./16.07.2019 Blockseminar

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.

Zeitplan

TBA

Themen

Nr. Thema Referent(in) Betreuer(in)
Modelle
1 Timed Automata Pia Halkour, Sebastian Scholz Jip Spel
2 Büchi Automata Loic Moison, Leonardo Pompe Shahid Khan
3 Markov Chains Anna Perret, Anubhav Punetha Sebastian Junges
4 Probabilistic Automata
5 (Dynamic) Fault Trees Konstantin Kaulen Sebastian Junges
Logiken
6 Hoare Logic Svenja Stein Jip Spel
7 Linear Temporal Logic
8 Computation Tree Logic
9 Separation Logic
10 Hennessy-Milner Logic Mayra Elwes, Dana Lenz Marcin Szymczak
Statische Analyseverfahren
11 Data-Flow Analysis Mattis Hoppe, Malik Ryskulbekov Sebastian Junges
12 Abstract Interpretation
13 Type Systems Daniel Shaolin Quirmbach, Erik Strobl Jip Spel
14 Pointer Analysis
15 Escape Analysis Dominik Lazar, Henrik Thillmann Thomas Noll
16 Shape Analysis Victor Czech, Mike Holtzem Thomas Noll
17 Inductive Invariants
18 Counterexample-Guided Abstraction Refinement (CEGAR)
Dynamische und Hybride Analyseverfahren
19 Runtime Verification Malcolm Burdorf, Jesse Germann Shahid Khan
20 Bounded Model Checking
21 Program Slicing Robin Lintermann, Jona Recker Sebastian Junges

Anmeldung

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

Weitere Informationen

Kontakt

Thomas Noll <noll at cs.rwth-aachen.de>