Sommersemester 2025
News
- 03.12.2024: Wir sind online!
Einführung und Themenvergabe
- Folien zur Einführung
- Formular zur Themenauswahl
Termine
| Anfang April 2025 | Einführungsveranstaltung |
| TBA | Frist für Themenauswahl |
| TBA | Letzte Rücktrittsmöglichkeit |
| TBA | Vorlage der detaillierten Vortragsstruktur |
| TBA | Vollständige Fassung der Folien |
| Mitte Juli 2025 | Blockseminar |
| TBA | Einreichung der Ausarbeitung |
Beachten Sie, dass die vollständige Fassung der Vortragsfolien Ihre zu bewertende Einreichung darstellt und sich von der endgültigen Version nur durch kleinere Anpassungen unterscheiden sollte, die nach Rücksprache mit der betreuenden Person erfolgen. Es ist aber möglich (und dringend empfohlen!), vor den jeweiligen Fristen Entwurfsversionen Ihrer Ergebnisse 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. | Thema | Studierende | Betreuer:In |
|---|---|---|---|
| Modelle | |||
| 1 | Timed Automata | – | – |
| 2 | Büchi Automata | – | – |
| 3 | Markov Chains | – | – |
| 4 | Probabilistic Automata | – | – |
| 5 | (Dynamic) Fault Trees | – | – |
| 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 | – | – |
| 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
- Artikel:
- 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 das zentrale SuPra-System. Nachträgliche Anmeldungen sind nicht möglich.
Weitere Informationen
- Muster zur Ausarbeitung
- Muster zu den Vortragsfolien
- How to Write a Seminar Paper
- How to give presentations
- Ethische Richtlinien für das Verfassen wissenschaftlicher Arbeiten
- Introduction to LaTeX
Kontakt
Thomas Noll <noll at cs.rwth-aachen.de>