E0 227 Program Analysis and Verification
August-December 2018, 3.30pm-5.00pm Mon Wed, Room 254
K. V. Raghavan,
Teaching assistants: Dr. Rekha Pai
(firstname.lastname@example.org), Stanly Samuel (email@example.com)
- Aug. 6: Introduction.
- Aug. 8, 13: Lattices.
- Aug. 20, 21: Introduction to
- Aug. 23, 27: Correctness of abstract
interpretation. Associated lecture
- Aug. 29, Sep. 3, 5: Kildall's algorithm.
- Sep. 10, 12: Inter-procedural analysis using
call strings approach.
- Sep. 17, 19, 24, 26: Inter-procedural analysis using functional
- Oct. 1, 3, 10: Inter-procedural analysis using IDFS approach.
- Oct. 12, 15, 17: Pointer analysis. Part 1 (pptx), Part 1 (pdf). Part 2 (pptx), Part 2 (pdf).
- Oct. 22, 24, 29: PDGs and slicing.
- Oct. 31, Nov. 5, Nov. 7: Floyd-Hoare logic.
- Nov. 14, 20, 27:: Simply Typed Lambda Calculus.
Program analysis is a collection of techniques for computing approximate
information about a program. Program analysis finds several applications:
in compilers, in tools that help programmers understand and modify
programs, and in tools that help programmers verify that programs satisfies
certain properties of interest. As software systems have become larger and
more complex there has been a lot of practical interest in using
program-analysis based tools to assist with software development. In this
course we will learn about techniques to reason about the meaning of and
the properties of a
program, and the
theory behind foundational program-analysis techniques such as abstract
interpretation, type systems, and theorem proving. We will also look at
an important application of program analysis, namely the operation of
We will assume that students have exposure to programming, the fundamental
concepts of programming languages, and the basics of mathematical logic and
discrete structures. However, no prior knowledge of program analysis is
Interpretation: Lattices, abstract join-over-all-paths analysis of a
program. Correctness of abstract information: Galois connections, abstract
interpretation as an over-approximation of concrete semantics. Dataflow
analysis: Computing an over-approximation of join-over-all-paths
information using Kildall's algorithm, by modeling the statements in the
program as a set of equations. Analysis of multi-procedure programs. Type
Systems: Monomorphic type systems. Pointer analysis of
imperative programs. Program slicing. Assertional reasoning using Hoare