Static Program Analysis

News

  • 2018-01-22: we are online!

Schedule

Type Day Time Hall Start Lecturer
Lecture Mon 14:15 – 15:45 AH 6 16 Apr Noll
  Tue 14:15 – 15:45 AH 2 17 Apr Noll
Exercise Tue 12:15 – 13:45 AH 2 24 Apr 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
1 16 Apr Introduction to Program Analysis l1 l1  
2 17 Apr Dataflow Analysis I (Introduction & Available Expressions/Live Variables Analysis) l2 l2 ex-01 
3 23 Apr Dataflow Analysis II (Algebraic Foundations) l3 l3  
4 24 Apr Dataflow Analysis III (The Framework) l4 l4 ex-02 
5 07 May Dataflow Analysis IV (MOP Solution) l5 l5  
6 08 May Dataflow Analysis V (MOP vs. Fixpoint Solution) l6 l6  
7 14 May Dataflow Analysis VI (Widening and Narrowing) l7 l7  
8 15 May Dataflow Analysis VII (DFA with Conditional Branches) l8 l8  
9 28 May Dataflow Analysis VIII (Java Bytecode Verification) l9 l9  
10 29 May Abstract Interpretation I (Galois Connections) l10 l10  
11 04 Jun Abstract Interpretation II (Safe Approximation) l11 l11  
12 05 Jun Abstract Interpretation III (Abstract Semantics of WHILE) l12 l12  
13 11 Jun Abstract Interpretation IV (Application Example: 16-Bit Multiplication) l13 l13  
14 12 Jun Abstract Interpretation V (Predicate Abstraction) l14 l14  
15 18 Jun Abstract Interpretation VI (Counterexample-Guided Abstraction Refinement) l15 l15  
16 19 Jun Abstract Interpretation VII (Limits & Improvements of CEGAR) l16 l16  
17 25 Jun Interprocedural Dataflow Analysis I (MVP Solution) l17 l17  
18 26 Jun Interprocedural Dataflow Analysis II (Fixpoint Solution) l18 l18  
19 02 Jul Pointer & Shape Analysis I l19 l19  
20 03 Jul Pointer & Shape Analysis II l20 l20  
21 09 Jul Wrap-Up l21 l21  

Exam

  • The exam will be offered in written or oral form, depending on the number of prospective participants. Details will be announced in the first lecture.
  • Students who intend to take an advanced master exam (“vorgezogene Masterprüfung”) need to register in person at ZPA. More information is available here.

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