News

      • Here you can find out how many exercise points you currently have.
      • 2013-01-16: A correction of exercise sheet 11, Ex. 3 is uploaded. Here you should prove that label 12 (not 11!) is not reachable.
      • Sheet 7 was updated to be consistent with notation from the lecture (at 13:30, Dec 5).
      • Note: There will be no exercise class on December 11th. Instead, the solutions to sheet 7 and 8 have to be handed in before the exercise class on December 18th.
      • 2012-11-05: correction of Example 4.4(2): the set of non-positive integer numbers (ordered by ≤) is not a complete lattice as ∅ does not have a least upper bound.
      • 2012-10-09: Added a short note to Ex. 1a!
      • 2012-10-18: all Wednesday lectures will take place in PPS H2, and all Thursday lectures will take place in 5052. The latter are shifted to 11:45-13:15.
      • 2012-06-15: we are online.


      Schedule

      Type

      Day

      Time

      Location

      Start

      Lecturer

      V3

      Wed

      10:00-11:30

      PPS H2 (until Nov 28)

      AH 2 (from Dec 12)

      Oct 10

      Noll

      Thu

      11:45-13:15

      5052

      Oct 18

      Noll

      Ü2

      Tue

      11:45-13:15

      AH 6

      Oct 23

      Dehnert, Jansen


      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 pointer-manipulating programs
      • 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)
      • Knowledge in the area of Theory of Programming (such as Semantics of Programming Languages or Software Verification) is helpful but not mandatory


      Slides

      Lecture

      Date

      Subject

      Slides

      Handout

      1

      Wed Oct 10

      Introduction to Program Analysis

      2

      Thu Oct 18

      Dataflow Analysis I

      (Introduction & Available Expressions Analysis)

      3

      Wed Oct 24

      Dataflow Analysis II

      (Live Variables Analysis)

      4

      Wed Oct 31

      Dataflow Analysis III

      (The Framework)

      5

      Thu Nov 8

      Dataflow Analysis IV

      (Worklist Algorithm & MOP Solution)

      6

      Wed Nov 14

      Dataflow Analysis V

      (Constant Propagation & Undecidability of MOP Solution)

      7

      Thu Nov 15

      Dataflow Analysis VI

      (MOP vs. Fixpoint Solution & Non-ACC Domains)

      8

      Wed Nov 21

      Dataflow Analysis VII

      (Interval Analysis, Widening & Narrowing)

      9

      Thu Nov 22

      Dataflow Analysis VIII

      (DFA with Conditional Branches)

      10

      Wed Nov 28

      (PPS H2)

      Dataflow Analysis IX

      (The Java Virtual Machine)

      11

      Thu Nov 29

      Dataflow Analysis X

      (Java Bytecode Verification)

      12

      Wed Dec 12

      (AH 2)

      Abstract Interpretation I

      (Theoretical Foundations)

      13

      Thu Wed 13

      Abstract Interpretation II

      (Abstract Semantics of WHILE)

      14

      Wed Dec 19

      Abstract Interpretation III

      (Abstract Interpretation of WHILE Programs)

      15

      Thu Dec 20

      Abstract Interpretation IV

      (Abstract Semantics and its Correctness)

      16

      Wed Jan 09

      Abstract Interpretation V

      (Application Example: 16-Bit Multiplication)

      17

      Thu Jan 10

      Abstract Interpretation VI

      (Predicate Abstraction)

      18

      Wed Jan 16

      Abstract Interpretation VII

      (Counterexample-Guided Abstraction Refinement)

      19

      Thu Jan 17

      Extensions I

      (Final Remarks on CEGAR & Interprocedural DFA)

      20

      Wed Jan 23

      Extensions II

      (Interprocedural DFA - MVP Solution)

      21

      Thu Jan 24

      Extensions III

      (Interprocedural DFA - Fixpoint Solution)

      22

      Wed Jan 30

      Extensions IV

      (Shape Analysis & Wrap-Up)


      Exam

      Exams are organized in oral form. The current schedule can be found in this spreadsheet.


      Further information

      • Depending on the audience, the course will be given in English or German. 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 vs. written) will be announced in the beginning of the course.


      Exercises

      The exercises are to be solved in groups of 2 and have to be handed in until the exercise class begins on tuesdays. In order to participate in the exam, you have to get at least 50% of the total sum of all exercise points.

       

      Exercise Sheets

       

      The exercise will take place on the following dates:

      • 23.10.
      • 30.10.
      • 13.11.
      • 20.11.
      • 27.11.
      • 04.12.
      • 18.12.
      • 08.01.
      • 15.01.
      • 22.01.
      • 29.01.

       

       


      Evaluation results


      Background literature and interesting links