- 2017-02-23: The exam inspection takes place on Wednesday, 1st March at 10:00 in the seminar room of i2 (E1, room 4201b).
- 2017-02-20: Added information about the rooms for the first exam (see below).
- 2017-01-30: fix(S) in exercise 12 denotes the least fixed point according to the new equation system in lecture 19.
- 2016-11-25: Fixed a typo in the example of exercise sheet 6, task 3.
- 2016-11-17: The lecture scheduled for Thu 01.12.2016 is shifted to Tue 06.12.2016 and will take place in AH 2.
- 2016-10-28: To clarify the second task of the second exercise sheet: The graphs under consideration contain an arrow from x to y if and only if y <= x and there is no z such that y < z < x.
- 2016-10-28: Small correction in the third exercise of the second exercise sheet.
- 2016-10-27: Due to the large number of participants to be expected, the exam will be organised in written form (for details see below)
- 2016-10-25: You can hand in your solutions to the exercises at the beginning of the exercise class. Alternatively, you can put your solutions into the box labeled ‘Static Program Analysis’ at the chair (E1, 2nd floor)
- 2016-07-26: we are online!
|Lecture||Tue||10:15 – 11:45||AH 1||18 Oct||Noll|
|Thu||10:15 – 11:45||AH 6||20 Oct||Noll|
|Exercise||Wed||12:00-13:30||AH 3||26 Oct||Jansen, Matheja|
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
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
|1||18 Oct||Introduction to Program Analysis||l1||l1|
|2||20 Oct||Dataflow Analysis I (Introduction & Available Expressions/Live Variables Analysis)||l2||l2||ex01|
|3||25 Oct||Dataflow Analysis II (Order-Theoretic Foundations)||l3||l3|
|4||27 Oct||Dataflow Analysis III (The Framework)||l4||l4||ex02|
|5||03 Nov||Dataflow Analysis IV (Worklist Algorithm & MOP Solution)||l5||l5||ex03|
|6||10 Nov||Dataflow Analysis V (MOP vs. Fixpoint Solution)||l6||l6||ex04|
|7||15 Nov||Dataflow Analysis VI (Undecidability of MOP Solution & Non-ACC Domains)||l7||l7||ex05|
|8||17 Nov||Dataflow Analysis VII (Narrowing & DFA with Conditional Branches)||l8||l8|
|9||22 Nov||Dataflow Analysis VIII (Conditional Interval Analysis & Java Virtual Machine)||l9||l9||ex06|
|10||24 Nov||Dataflow Analysis IX (Java Bytecode Verification)||l10||l10|
|11||29 Nov||Abstract Interpretation I (Theoretical Foundations)||l11||l11||ex07|
|12||06 Dec (AH 2!)||Abstract Interpretation II (Safe Approximation)||l12||l12||ex08|
|13||13 Dec||Abstract Interpretation III (Abstract Semantics of WHILE)||l13||l13||ex09|
|14||15 Dec||Abstract Interpretation IV (Application Example: 16-Bit Multiplication)||l14||l14|
|15||20 Dec||Abstract Interpretation V (Numerical & Predicate Abstraction)||l15||l15||ex10|
|16||10 Jan||Abstract Interpretation VI (Counterexample-Guided Abstraction Refinement)||l16||l16|
|17||12 Jan||Abstract Interpretation VII (Limits and Improvements of CEGAR)||l17||l17||ex11|
|18||17 Jan||Interprocedural Dataflow Analysis I (MVP Solution)||l18||l18|
|19||19 Jan||Interprocedural Dataflow Analysis II (Fixpoint Solution)||l19||l19||ex12|
|20||31 Jan||Wrap-Up Interprocedural DFA & Pointer Analysis||l20||l20|
|21||02 Feb||Shape Analysis & Final Remarks||l21||l21|
|–||08 Feb (12:00, AH 3)||Exam Preparation||–||–|
- Written exams:
- Students who intend to take an advanced master exam (“vorgezogene Masterprüfung”) need to register in person at ZPA. More information is available here.
- The lectures will be given in German or English, depending on the language proficiency of the audience.
- The slides and other course material will be in English. There are no lecture notes (yet); the course material will consist of slides.
- The form of the exam (oral/written) will be announced in the beginning of the course.
Background Literature and Interesting Links
- Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis. 2nd edition, Springer, 2005 [available in CS Library]
- 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]
- X. Leroy: Java Bytecode Verification: Algorithms and Formalizations,
Journal of Automated Reasoning 30(3-4), 2003, 235-269
- J. Knoop, B. Steffen: The Interprocedural Coincidence Theorem, Proc. CC ’92, LNCS 641, Springer, 1992, 125-140
- 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
- Berkeley Lazy Abstraction Software Verification Tool (BLAST)
- SLAM Model Checker
- Collatz Conjecture