Proseminar, Sommersemester 2022
News
- 25.11.2021: Wir sind online!
Termine
| 4. April | Einführungsvideo online |
| 11. April | Frist für Themenauswahl |
| 6. Mai | Letzte Rücktrittsmöglichkeit |
| 9. Mai | Vorlage der detaillierten Inhaltsübersicht |
| 7. Juni | Vollständige Fassung der Ausarbeitung |
| 27. Juni | Vollständige Fassung der Vortragsfolien |
| 11. Juli | Seminarvorträge (Raum 9U10, Gebäude E3) |
| 18. Juli | Finale Revision der Ausarbeitung |
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.
Einführung und Themenvergabe
- Video zur Einführung
- Folien zur Einführung
- Foodle-Umfrage zur Themenvergabe
- Schulung in Literaturrecherche
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 | Montag, 11. Juli |
| 10:00 – 10:40 | Finn Henning, Leon Streichardt |
| 14:00 – 15:00 | Julius Hündlings, Mohamed Aziz El Hammi, Ana Poput |
Themen
| Nr. | Thema | StudentIn | BetreuerIn |
|---|---|---|---|
| Modelle | |||
| 1 | Timed Automata | – | – |
| 2 | Büchi Automata | – | – |
| 3 | Markov Chains | Finn Henning, Julius Hündlings | Lutz Klinkenberg |
| 4 | Probabilistic Automata | – | – |
| 5 | (Dynamic) Fault Trees | Daniel Braun, Mohamed Aziz El Hammi | Alexander Bork |
| Logiken | |||
| 6 | Hoare Logic | – | – |
| 7 | Linear Temporal Logic | – | – |
| 8 | Computation Tree Logic | – | – |
| 9 | Separation Logic | – | – |
| 10 | Hennessy-Milner Logic | – | – |
| Statische Analyseverfahren | |||
| 11 | Data-Flow Analysis | Ana Poput, Leon Streichardt | Thomas Noll |
| 12 | Abstract Interpretation | – | – |
| 13 | Type Systems | – | – |
| 14 | Pointer Analysis | – | – |
| 15 | Escape Analysis | – | – |
| 16 | Shape Analysis | – | – |
| 17 | Inductive Invariants | – | – |
| 18 | Counterexample-Guided Abstraction Refinement (CEGAR) | – | – |
| Dynamische und Hybride Analyseverfahren | |||
| 19 | Runtime Verification | – | – |
| 20 | Bounded Model Checking | – | – |
| 21 | Program Slicing | – | – |
Literatur
- C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Section 9.1: Timed Automata
- R. Alur: Timed automata. CAV 1999
- W. Thomas: Automata on infinite objects. In Handbook of Theoretical Computer Science, Elsevier, 1990
- C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Section 10.1: Markov Chains
- M. O. Rabin: Probabilistic Automata. Information & Control 1963
- E. Ruijters, M. Stoelinga: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer Science Review 2015
- Mike Gordon: Background reading on Hoare Logic. Lecture notes, 2015
- C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Chapter 5: Linear Temporal Logic
- C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Chapter 6: Computation Tree Logic
- P. W. O’Hearn: A Primer on Separation Logic (and Automatic Program Verification and Analysis). Software Safety and Security; Tools for Analysis and Verification, 2012
- Matthew Hennessy, Robin Milner: Algebraic laws for nondeterminism and concurrency, Journal of the ACM, 1985
- A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 5: Dataflow Analysis with Monotone Frameworks
- A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 11: Abstract Interpretation
- A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 3: Type Analysis
- A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 10: Pointer Analysis
- J.-D. Choi, M. Gupta, M. Serrano, V. C. Sreedhar, S. Midkiff: Escape analysis for Java. OOPSLA 1999
- R. Wilhelm, M. Sagiv, T. Reps: Shape Analysis. CC 2000
- A. R. Bradley: Understanding IC3. SAT 2012
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 2003
- E. Bartocci, Y. Falcone, A. Francalanza, G. Reger: Introduction to Runtime Verification. Lectures on Runtime Verification 2018
- E. Clarke, A. Biere, R. Raimi, Y. Zhu: Bounded Model Checking Using Satisfiability Solving. FMSD 2001
- M. Harman, R. Hierons: An overview of program slicing. Software Focus 2002
Anmeldung
Die Anmeldung erfolgt über eine zentrale Seite der Fachgruppe Informatik. Nachträgliche Anmeldungen sind nicht möglich.
Bewertung
Das Bewertungs-Schema ist hier verfügbar: https://moves.rwth-aachen.de/wp-content/uploads/proseminar_grading_scheme.pdf
Weitere Informationen
- Vorlage zur Ausarbeitung
- Vorlage zu den Vortragsfolien
- Hinweise zur Anfertigung der Ausarbeitung
- How to give presentations
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten