Proseminar Introduction to Program Analysis

Sommersemester 2025

News

  • 03.12.2024: Wir sind online!

Einführung und Themenvergabe

Termine

Mi, 16. April, 16:30 UhrEinführungsveranstaltung (Seminarraum 4201b, 2. Stock, Gebäude E1, Informatikzentrum)
22. AprilFrist für Themenauswahl
30. AprilLetzte Rücktrittsmöglichkeit
19. MaiVorlage der detaillierten Vortragsstruktur
16. JuniVollständige Fassung der Folien
15. Juli (?)Blockseminar
28. JuliEinreichung 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.ThemaStudierendeBetreuende
Modelle
1Timed Automata––
2Büchi Automata––
3Markov Chains––
4Probabilistic Automata––
5(Dynamic) Fault Trees––
Logiken
6Hoare Logic––
7Linear Temporal LogicLaszlo HinzLena Verscht
8Computation Tree Logic––
9Separation Logic––
Statische Analyseverfahren
10Data-Flow Analysis––
11Abstract Interpretation––
12Pointer Analysis––
Dynamische und Hybride Analyseverfahren
13Runtime VerificationAndra-Maria RujaLena Verscht
14Program SlicingRayLena Verscht

Literatur

  1. Artikel:
    • C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Section 9.1: Timed Automata
    • R. Alur: Timed automata. CAV 1999
  2. W. Thomas: Automata on infinite objects. In Handbook of Theoretical Computer Science, Elsevier, 1990
  3. C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Section 10.1: Markov Chains
  4. M. O. Rabin: Probabilistic Automata. Information & Control 1963
  5. E. Ruijters, M. Stoelinga: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer Science Review 2015
  6. Mike Gordon: Background reading on Hoare Logic. Lecture notes, 2015
  7. C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Chapter 5: Linear Temporal Logic
  8. C. Baier, J.-P. Katoen: Principles of Model Checking. MIT Press 2008. Chapter 6: Computation Tree Logic
  9. 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
  10. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 5: Dataflow Analysis with Monotone Frameworks
  11. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 12: Abstract Interpretation
  12. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 11: Pointer Analysis
  13. E. Bartocci, Y. Falcone, A. Francalanza, G. Reger: Introduction to Runtime Verification. Lectures on Runtime Verification 2018
  14. 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

Kontakt

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