Static Program Analysis

News

  • 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!

Schedule

Type Day Time Hall Start Lecturer
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

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

Slides

No. Date Subject Slides Handout Exercises Solutions
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  –  –    

Exam

Evaluation results

Further information

  • 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