Introduction to Program Analysis (Proseminar)

Sommersemester 2021

News

  • 23.12.2020: Wir sind online!

Termine

13.04.2021, 14:00Einführungsveranstaltung (Zoom-Meeting)
18.04.2021Frist für Themenauswahl
10.05.2021Letzte Rücktrittsmöglichkeit
10.05.2021Vorlage der detaillierten Inhaltsübersicht
07.06.2021Vollständige Fassung der Ausarbeitung
28.06.2021Vollständige Fassung der Vortragsfolien
12.07.2021Seminarvorträge

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

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

ZeitMontag, 12. Juli
10:00-11:00Fatih Batuhan Kablan, Noah Dill, Siming Lau
11:30-12:10Cedric Dückers, Mert Saglam

Themen

Nr.ThemaStudentInBetreuerIn
Modelle
1Timed AutomataFatih Batuhan KablanTim Quatmann
2Büchi AutomataNoah Dill, Cedric DückersLutz Klinkenberg
3Markov Chains––
4Probabilistic Automata––
5(Dynamic) Fault TreesSiming Lau, Mert SaglamThomas Noll
Logiken
6Hoare Logic––
7Linear Temporal Logic––
8Computation Tree Logic––
9Separation Logic––
10Hennessy-Milner Logic––
Statische Analyseverfahren
11Data-Flow Analysis––
12Abstract Interpretation––
13Type Systems––
14Pointer Analysis––
15Escape Analysis––
16Shape Analysis––
17Inductive Invariants––
18Counterexample-Guided Abstraction Refinement (CEGAR)––
Dynamische und Hybride Analyseverfahren
19Runtime Verification––
20Bounded Model Checking––
21Program 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
  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. Matthew Hennessy,  Robin Milner: Algebraic laws for nondeterminism and concurrency, Journal of the ACM, 1985
  11. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 5: Dataflow Analysis with Monotone Frameworks
  12. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 11: Abstract Interpretation
  13. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 3: Type Analysis
  14. A. Møller and M. I. Schwartzbach: Static Program Analysis. Lecture notes, 2020. Chapter 10: Pointer Analysis
  15. J.-D. Choi, M. Gupta, M. Serrano, V. C. Sreedhar, S. Midkiff: Escape analysis for Java. OOPSLA 1999
  16. R. Wilhelm, M. Sagiv, T. Reps: Shape Analysis. CC 2000
  17. A. R. Bradley: Understanding IC3. SAT 2012
  18. E. Clarke,  O. Grumberg,  S. Jha,  Y. Lu,  H. Veith: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 2003
  19. E. Bartocci, Y. Falcone, A. Francalanza, G. Reger: Introduction to Runtime Verification. Lectures on Runtime Verification 2018
  20. E. Clarke, A. Biere, R. Raimi, Y. Zhu: Bounded Model Checking Using Satisfiability Solving. FMSD 2001
  21. 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.

Weitere Informationen

Kontakt

Thomas Noll