Master course in Summer 2022
News
- 2021-12-16: We are online!
Schedule
| Type | Day | Time | Room | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture | Mon | 12:30-14:00 | AH 1 | 25 Apr | Noll |
| Tue | 14:30-16:00 | AH 2 | 19 Apr | Noll | |
| Exercise | Fri | 10:30-12:00 | AH 3 | 29 Apr | Batz/Winkler |
Contents
The goal of this course is to introduce foundational methods and techniques for analysing software on source-code level. The following topics will be discussed:
- Dataflow analysis
- Abstract interpretation
- Interprocedural analysis
- Analysis of heap data structures
- Applications in optimising compilers and software verification
Prerequisites
Basic knowledge of the following relevant undergraduate courses is expected:
- Programming (essential concepts of imperative and object-oriented programming languages and elementary programming techniques)
- Formal Languages and Automata Theory (regular and context-free languages, finite and pushdown automata)
- Knowledge in the area of Theory of Programming (such as Semantics of Programming Languages or Software Verification) is helpful but not mandatory
Organisation
TBA
Lecture Material and Exercises
All material is available from the associated RWTHmoodle classroom after registration via RWTHonline.
Exam
- The exam will be offered in written or oral form, depending on the number of prospective participants. Details will be announced later.
- There are no specific admission requirements.
Background Literature and Interesting Links
- General:
- Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis. 2nd edition, Springer, 2005 [available in CS Library]
- Anders Møller and Michael I. Schwartzbach: Lecture Notes on Static Analysis
- Helmut Seidl, Reinhard Wilhelm, Sebastian Hack: Übersetzerbau 3: Analyse und Transformation. Springer, 2010 [available in CS Library]
- Steven S. Muchnick, Neil D. Jones: Program Flow Analysis: Theory and Applications. Prentice Hall, 1981 [available in CS Library]
- Bytecode verificaton:
- X. Leroy: Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning 30(3-4), 2003, 235-269
- J. Chrząszcz, P. Czarnik, A. Schubert: A Dozen Instructions Make Java Bytecode, Electronic Notes in Theoretical Computer Science 264(4), 2011, 19-34
- Interprocedural dataflow analysis:
- J. Knoop, B. Steffen: The Interprocedural Coincidence Theorem, Proc. CC ’92, LNCS 641, Springer, 1992, 125-140
- Tools:
- P. Emanuelsson, U. Nilsson: A Comparative Study of Industrial Static Analysis Tools, Technical Report 2008:3, Linköping University, Sweden, 2008
- Wikipedia List of Tools for Static Code Analysis
- CPAchecker
- SLAM Model Checker
- Attestor: A Shape Analysis Tool based on Graph Grammars
- Miscellaneous: