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)