Program Analysis

Shmuel (Mooly) Sagiv Sunday 16-17 Shenkar 204

Advanced techniques for statically analyzing programs are discussed. These techniques allows one to answer computationally hard questions about programs in an efficient albeit conservative way. They are also referred to as abstract interpretation since the algorithms interpret the program on a simplified abstract domain. The techniques are useful in compilers in order to generate more efficient code and in other programming language environments such as debuggers and code quality checkers.

For an interesting note on static analysis click here.

Important Message

If your POWERPOINT does not show certain mathematical characters use fonts in a zip file, by clicking here. Make sure to extract
them to the appropriate directory,

Alternatively, you can extract them anywhere, and install them via the control panel

Contents

Example Program Analysis Problems


Course Requirements

Bibliography

The course book Principles of Program Analysis by Nielson, Nielson and Hankin is available in Dionon.

Course Schedule

  1. Course Overview
    Printer Friendly Version
    Class Summary by Oded Elbaz and Tomer Greenwald
    Class Summary by Oded Elbaz and Tomer Greenwald (sources)
  2. Chaotic Iterations
    Printer Friendly Version
    Class Summary by Yuval Rochman and Michal Shagam
  3. Chaotic Iterations Example
    Printer Friendly Version
    Introduction to Abstract Interpretation
    Printer Friendly Version
    Class Summary by Dor Wucher and Yael Tiomkin
  4. Numerical Abstract Interpretation
    Printer Friendly Version
    Original Slides due to Antione Mine
    Class Summary by Omer Anson and Shelly Grossman
  5. Detecting Buffer Overruns in C Programs
    Printer Friendly Version
    Class Summary by Misha Seltzer
  6. Combining Abstract Domains
    Printer Friendly Version
    Class Summary by Keren Zubovsky and Orit Sanandaji
  7. Interprocedural Analysis
    Printer Friendly Version
  8. Automating Abstract Interpretation
    Printer Friendly Version
  9. Counterexample Guided Abstract Refinement
    Printer Friendly Version
    Class Summary by Asya Frumkin and Aviv Kuvent
  10. Shape Analysis
    Printer Friendly Version
    Class Summary by Gal Dudovitch and Daniela Rabkin
  11. The LLVM Inferastructure
    Printer Friendly Version
  12. Static Analysis of Java
    Printer Friendly Version

Homework Assignments

Assignment 1: Due December 20
Assignment 2: Due January 30

For further information Email:msagiv@post.tau.ac.il