Proseminar, Wintersemester 2016/17
News
- 23.06.2016: Wir sind online!
Termine
| 21.10.2016, 12:30 | Einführungsveranstaltung im Seminarraum 5054 (Informatikzentrum) |
| 11.11.2016 | Letzte Rücktrittsmöglichkeit |
| 28.11.2016 | Vorlage der detaillierten Inhaltsübersicht |
| 13.12.2016, 15:30 oder 15.12.2016, 09:00 oder 19.12.2016, 16:30 | Einführung in die Literaturrecherche (Informatik-Bibliothek) |
| 09.01.2017 | Vollständige Fassung der Ausarbeitung |
| 30.01.2017 | Vollständige Fassung der Folien |
| 06./07.02.2017, jeweils ab 09:00 | Blockseminar (Informatikzentrum 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 mathematischen 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 | Montag | Dienstag |
|---|---|---|
| 09:00-10:30 | Ibach, Murad Oli, Yilmaz | Gehrke, Frenz, Zelmat |
| 10:45-12:15 | Hense, Pinders, Schlein | Pförtner, Lingeswaran, Kreiger |
| 14:00-15:30 | Zhang, Tegtmeier, Schröer | Behrens, Quirl, Johnen |
| 15:45-16:45 | – | Oelgemöller, Jonalik |
Themen
| Nr. | Thema | Referent(in) | Betreuer(in) |
|---|---|---|---|
| Modelle | |||
| 1 | Timed Automata | Julius Hense, Marvin Pförtner | Sebastian Junges |
| 2 | Büchi Automata | Jan-Niklas Gehrke, Alina Ibach | Christian Dehnert |
| 3 | Markov Chains | – | – |
| 4 | Probabilistic Automata | Simon Frenz, Wahid Murad Oli | Christian Dehnert |
| 5 | (Dynamic) Fault Trees | Janusan Lingeswaran, Erik Pinders | Sebastian Junges |
| Logiken | |||
| 6 | Hoare Logic | – | – |
| 7 | Linear Temporal Logic | Serkan Yilmaz, Oliver Zelmat | Tim Quatmann |
| 8 | Computation Tree Logic | – | – |
| 9 | Separation Logic | – | – |
| 10 | Hennessy-Milner Logic | – | – |
| Statische Analyseverfahren | |||
| 11 | Data-Flow Analysis | Florian Behrens | Tim Lange |
| 12 | Abstract Interpretation | – | – |
| 13 | Type Systems | – | – |
| 14 | Points-to Analysis | – | – |
| 15 | Alias Analysis | Torben Oelgemöller, Philipp Schröer | Harold Bruintjes |
| 16 | Escape Analysis | – | – |
| 17 | Shape Analysis | Nils Jonalik | Harold Bruintjes |
| 18 | Inductive Invariants | – | – |
| 19 | Counterexample-Guided Abstraction Refinement (CEGAR) | – | – |
| Dynamische Analyseverfahren | |||
| 20 | Runtime Verification | Sergej Kreiger, Steffan Schlein | Thomas Noll |
| 21 | Bounded Model Checking | – | – |
| 22 | Profiling | Domenic Quirl, Hengwen Zhang | Thomas Noll |
| Hybride Analyseverfahren | |||
| 23 | Program Slicing | Tobias Johnen, Alexander Tegtmeier | Tim Lange |
Anmeldung
Die Anmeldung erfolgt zwischen dem 24. Juni und dem 10. Juli 2016 über die zentrale Fachgruppenseite. Nachträgliche Anmeldungen sind nicht möglich.
Weitere Informationen
Kontakt
Thomas Noll <noll at cs.rwth-aachen.de>