Proseminar, Sommersemester 2019
News
- Der erste Tag des Blockseminars wird von Montag auf Donnerstag verlegt; entsprechend findet dieses am 16. und 18. Juli statt.
- 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 | ||||
|
Einführung in die Literaturrecherche (Informatik-Bibliothek) | ||||
| 23.06.2019 | Vollständige Fassung der Ausarbeitung | ||||
| 07.07.2019 | Vollständige Fassung der Folien | ||||
| 16./18.07.2019 | Blockseminar im Seminarraum Informatik 2 (Gebäude E1, Raum 4201b |
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
| Zeit | Di, 16. Juli | Do, 18. Juli |
|---|---|---|
| 09:00-10:00 | Dana Lenz, Dominik Lazar, Victor Czech | Mayra Elwes, Henrik Thillmann, Mike Holtzem |
| 10:15-11:15 | Pia Halkour, Svenja Stein, Daniel Shaolin Quirmbach | Sebastian Scholz, Erik Strobl, Konstantin Kaulen |
| 11:30-12:10 | Leonardo Pompe, Jesse Germann | Loic Moison, Malcolm Burdorf |
| 13:00-14:00 | Anna Perret, Mattis Hoppe, Robin Lintermann | Anubhav Punetha, Malik Ryskulbekov, Jona Recker |
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>