News

      • 2011-07-01: evaluation results are online
      • 2011-03-08: page set up


      Schedule

      Type

      Day

      Time

      Location

      Start

      Lecturer

      V3

      Wed

      10:00-11:30

      AH 6

      Apr 6

      Noll

      Thu

      15:00-16:30 (bi-weekly)

      AH 5

      Apr 14

      Noll

      Ü2

      Mon

      10:00-11:30

      AH 2

      Apr 18

      Heinen/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
      • Constraint-based analysis
      • 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 Apr 6

      Introduction to Program Analysis

      2

      Wed Apr 13

      Dataflow Analysis I

      (Introduction & Available Expressions Analysis)

      3

      Thu Apr 14

      Dataflow Analysis II

      (Live Variables Analysis)

      4

      Wed Apr 20

      Dataflow Analysis III

      (The Framework)

      5

      Wed Apr 27

      Dataflow Analysis IV

      (Worklist Algorithm & MOP Solution)

      6

      Thu Apr 28

      Dataflow Analysis V

      (Constant Propagation & Undecidability of MOP Solution)

      7

      Wed May 4

      Dataflow Analysis VI

      (MOP vs. Fixpoint Solution)

      8

      Wed May 11

      Dataflow Analysis VII

      (Interval Analysis & Widening)

      9

      Thu May 12

      Dataflow Analysis VIII

      (Narrowing & DFA with Conditional Branches)

      10

      Wed May 18

      Dataflow Analysis IX

      (The Java Bytecode Verifier)

      11

      Wed May 25

      Dataflow Analysis X

      (Java Bytecode Verification)

      12

      Thu May 26

      Abstract Interpretation I

      (Theoretical Foundations)

      13

      Wed Jun 1

      Abstract Interpretation II

      (Abstract Semantics of WHILE)

      14

      Wed Jun 8

      Abstract Interpretation III

      (Abstract Interpretation of WHILE Programs)

      15

      Thu Jun 9

      Abstract Interpretation IV

      (Correctness of Abstract Semantics)

      16

      Wed Jun 22

      Abstract Interpretation V

      (Application Example: 16-Bit Multiplication)

      17

      Wed Jun 29

      Abstract Interpretation VI

      (Predicate Abstraction)

      18

      Thu Jun 30

      Abstract Interpretation VII

      (Counterexample-Guided Abstraction Refinement)

      19

      Wed Jul 6

      Extensions I

      (Interprocedural Dataflow Analysis - MVP Solution)

      20

      Wed Jul 13

      Extensions II

      (Interprocedural Dataflow Analysis - Fixpoint Solution)

      21

      Thu Jul 14

      Extensions III

      (Pointer Analysis & Wrap-Up)


      Exercise sheets

      Exercise sheets will be made available on Mondays. The deadline for handing in your solution is on Mondays, before the exercise class begins.


      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/written) will be announced in the beginning of the course.


      Evaluation results


      Background literature and interesting links