Program Analysis

CSC2125F: Topics in Software Engineering (Fall 2009)


Lectures

Week (1): Introduction (pdf)
Week (2): Data Flow Analysis.
See these slides as a concise reference, and these slides as a more detailed reference.
Read chapter 2 of this book to fill in the gaps.
Week (3): Interprocedural Data Flow Analysis.
Read this paper as the main reference.
Week (4): Abstraction: Galois Connection and Closure Operators (pdf).
Week (5): Abstraction continued (pdf).
week (6): Program Semantics (pdf).
week (7): Program Properties and Program Logics (pdf).
week (8): Safety and Liveness Categorization of Properties.
Week (9): Abstraction Examples and Abstract Interpretation Overview.
week (10): Abstract Interpretation.
Have a look at these slides as supplementary material.
week (11): Predicate Abstraction.
It was introduced by Graf and Saidi. Here is an extension which is applicable to real software.
week (12): Model Checking
A reference for LTL to Automata Construction.
week (13): μ-calculus
A reasonable reference.

Announcements

Lectures are held at 2-4pm in BA 3201.

Assignment (1) is out and due on October 22nd (in class).
Assignment (2) is out and due on November 19th (in class).
Assignment (3) is out and due (with an extension) on December 20th.




Homework:

Assignment (1): Read this paper "Two approaches to interprocedural data flow analysis" by Sharir and Pnueli, and write a short summary of the "Call Strings" approach. It has to be good enough for someone who has not read the paper to understand what the approach is about.
Here is a link to an online library for this. I have made arrangments with Engineering and Computer Science Library for the book containing this essay to be on hold for the next two weeks. You can make copies of it if reading the paper online using the above link is not convenient. Here is a link to a pdf version (Thanks to Zuzel).

Also, write the proofs of the two cases tagged as exercise (with a red box!) in this lecture. The proofs should be precise, and each step of the deduction should have a short explanation; e.g. "by definition of galois connection", or "by extensiveness of the upper closure operator f".

Assignment (2)

Assignment (3)