Static Program Analysis

News

  • There will be a Q&A session on Tuesday, February 24, from 14:00 to 15:30 in the AH 6 lecture hall. In order to supply you with complete and comprehensible answers to your questions, we do ask that you send us your questions via email a few days beforehand, if possible.
  • Registration for an oral exam date is possible by 31 January via this poll.
  • There will be no exercise sheet from Mon 15 December to Mon 5 January. The next exercise sheet will be online from Mon 5 January and its solution will be presented in the exercise class on Mon 12 January. Consequently, there will be no exercise class on Mon 5 January.
  • There was a slight mistake in exercise 1 of sheet 1. The sheet was updated on Tuesday, 21 Oct, 19:08.
  • 2014-09-02: we are online!

Schedule

Type Day Time Hall Start Lecturer
Lecture Mon 14:15 – 15:45 AH 1 13 Oct Noll/Jansen
Thu 14:15 – 15:45 AH 2 16 Oct Noll/Jansen
Exercise Mon 10:15 – 11:45 AH 6 27 Oct Dehnert/Kaminski

Contents

The goal of this course is to introduce foundational methods and techniques for analyzing software on source-code level. The following topics will be discussed:
  • Dataflow analysis
  • Abstract interpretation
  • Interprocedural analysis
  • Analysis of heap data structures
  • Applications in optimizing 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 13 Oct Introduction to Program Analysis l1 l1
2 20 Oct Dataflow Analysis I
(Introduction & Available Expressions/Live Variables Analysis)		 l2 l2 e1 s1
3 23 Oct Dataflow Analysis II
(Order-Theoretic Foundations)		 l3 l3
4 27 Oct Dataflow Analysis III
(The Framework)		 l4 l4 e2 s2
5 30 Oct Dataflow Analysis IV
(Worklist Algorithm & MOP Solution)		 l5 l5 e3 s3
6 10 Nov Dataflow Analysis V
(MOP vs. Fixpoint Solution)		 l6 l6 e4 s4
7 13 Nov Dataflow Analysis VI
(Undecidability of MOP Solution & Non-ACC Domains)		 l7 l7
8 17 Nov Dataflow Analysis VII
(Narrowing & DFA with Conditional Branches)		 l8 l8 e5 s5
9 20 Nov Dataflow Analysis VIII
(Conditional Interval Analysis & Java Virtual Machine)		 l9 l9
10 24 Nov Dataflow Analysis IX
(Java Bytecode Verification)		 l10 l10 e6 s6
11 27 Nov Abstract Interpretation I
(Theoretical Foundations)		 l11 l11
12 01 Dec Abstract Interpretation II
(Safe Approximation of Functions and Relations)		 l12 l12 e7 s7
13 08 Dec Abstract Interpretation III
(Abstract Interpretation of WHILE Programs)		 l13 l13 e8 s8
14 15 Dec Abstract Interpretation IV
(Application Example: 16-Bit Multiplication)		 l14 l14
– 18 Dec Cancelled – –
15 05 Jan Abstract Interpretation V
(Numerical & Predicate Abstraction)		 l15 l15 e9 s9
16 08 Jan Abstract Interpretation VI
(Counterexample-Guided Abstraction Refinement)		 l16 l16
17 12 Jan Abstract Interpretation VII
(Final Remarks on CEGAR)		 l17 l17 e10 (sources) s10
18 15 Jan Interprocedural Dataflow Analysis I
(MVP Solution)		 l18 l18
19 22 Jan Interprocedural Dataflow Analysis II
(Fixpoint Solution)		 l19 l19
20 26 Jan Wrap-Up Interprocedural DFA & Pointer Analysis l20 l20
21 29 Jan Shape Analysis & Final Remarks l21 l21

Exam

  • Please register for an oral exam date by 31 January via this poll.
  • Registration is possible via this Campus page.
  • Students who intend to take an advanced master exam (“vorgezogene Masterprüfung”) need to register in person at ZPA between December 8 and 18. More information is available here.
  • Exams take place in Thomas Noll’s office (E1, 2nd floor, room 4211) according to the following schedule:
    Date Time Student
    12 Mar 09:00-09:30 Thomas Mertens
    09:30-10:00 Frederick Prinz
    10:00-10:30 Stefan Kohnen
    10:30-11:00 –
    11:00-11:30 Thomas Schraut
    11:30-12:00 Thomas Henn
    12:00-12:30 Eric Marre
    12:30-14:00 –
    14:00-14:30 Johannes Krude
    14:30-15:00 Jan Bruckner
    15:00-15:30 Kilian Merkelbach
    15:30-16:00 Munkhzul Erdenedash
    24 Mar 09:00-09:30 Thomas Buning
    09:30-10:00 Yannick Deuster
    10:00-10:30 Jens Katelaan
    10:30-11:00 –
    11:00-11:30 Nico Wübbels
    11:30-12:00 Simeon Keller
    12:00-12:30 Florin Godard
    12:30-14:00 –
    14:00-14:30 Michael Deutschen
    14:30-15:00 Daniel Schiller
    15:00-15:30 Jan-Erik Rediger
    15:30-16:00 Andreas Guth
    08 Apr 09:00-09:30 Andre Mann
    09:30-10:00 Siamak Mottaghian
    10:00-10:30 Philipp Bock
    10:30-11:00 –
    11:00-11:30 Manuel Krebber
    11:30-12:00 Fabian Böller
    12:00-12:30 Sascha Müller
    12:30-14:00 –
    14:00-14:30 David Laukamp
    14:30-15:00 Oliver Ney
    15:00-15:30 Nico Friedrich
    15:30-16:00 Mateusz Buglowski
    16:00-16:30 Samiro Discher

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