E0 227 Program Analysis and Verification
August-December 2021, 3.30pm-5.00pm Mon Wed, Lectures link is available
K. V. Raghavan,
Teaching assistants: Alvin George (alvingeorge), Raseek C
- Aug. 3: Overview of all
three courses for 2021-22 academic year.
- Aug. 9: Introduction to this course.
- Aug. 11, 16: Lattice theory.
- Aug. 18, 23: Introduction to abstract interpretation.
- Aug. 25, 30: Correctness of abstract
interpretation. Associated lecture
- Sep. 1, 6, 8: Kildall's algorithm. Associated
- Sep. 13, 15, 20: Call
- Sep. 22, 27, Oct. 4: Functional
- Oct. 6, 8, 13: Pointer analysis. Part
1 (pptx), Part 2 (pptx).
1 (pdf), Part 2 (pdf).
- Oct. 18, 20, 25: Intraprocedural slicing
- Oct. 27, Nov. 8, 10: Floyd-Hoare logic
- Nov. 15, 17, 22: 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