E0 227 Program Analysis and Verification
August-December 2019, 3.30pm-5.00pm Tue Thu, Room 117
K. V. Raghavan,
Teaching assistants: Habeeb P
(firstname.lastname@example.org), Geetam Chawla (email@example.com)
- Aug. 8: Introduction.
- Aug. 13, 16: Lattices.
- Aug. 20, 22: Introduction to
- Aug. 27, 29: Correctness of abstract
interpretation. Associated lecture
- Sep. 3, 5: Kildall's algorithm.
- Sep. 12, 17: Inter-procedural analysis using the calls strings approach.
- Sep. 19, 24, 26: Inter-procedural analysis using the functional approach.
- Sep. 27, Oct. 3, 4: Inter-procedural analysis using the IDFS approach.
- Oct. 15, 17, 18: Points to analysis. Part 1 (pptx), Part 1 (pdf). Part 2 (pptx), Part 2 (pdf).
- Oct. 22, 24: Intra-procedural
- Oct. 27, 29, Nov. 5: Inter-procedural
- Nov. 7, and two more classes:
- Nov. 19, 21, 22: Simply Typed Lambda
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