Master course in Summer 2020
News
- 2020-04-01: all course-related material will be distributed via the RWTHmoodle classroom.
- 2020-03-24: until further notice, the course will be fully organised in electronic form, without in-class meetings. Please refer to the organisation section for further details.
- 2020-01-24: we are online!
Schedule
Type | Day | Time | Room | Start | Lecturer |
---|---|---|---|---|---|
Lecture | Mon | [ | Slidecast [ | 20 Apr | Noll |
Fri | [ | Slidecast [ | 24 Apr | Noll | |
Exercise | Mon | 14:30-16:00 | Video conference [ | 04 May | Batz/Szymczak |
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
Due to the Corona virus outbreak, no in-class meetings are currently possible. All course-related material will therefore be made accessible in electronic form:
- At the dates that were foreseen for lectures (or earlier), slidecasts and/or video recordings will be made available.
- Starting April 27, assignment sheets are made available weekly via web, with a submission deadline of one week.
- Paper submissions are not accepted; everything has to be (scanned and) submitted via RWTHmoodle.
- The presentations of sample solutions will be organised as video conferences on the date of the exercise class (one week after the publication of the assignment sheet).
- Exercises are optional, i.e., not required for admission to exams. However, corrections to students’ solutions are provided as annotations to the submissions.
Lecture Material and Exercises
All material is available from the 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: