Program Analysis and Verification

E0 227 Program Analysis and Verification

August-December 2023, 3:30 pm - 5 pm Mon Wed, Room 117, CSA

Instructors: K. V. Raghavan, Deepak D'Souza

Teaching assistants: Abhishek Uppar (abhisheku), Devansh Tyagi (devanshtyagi)

Lectures

Aug. 2: Introduction
Aug. 7, 9: Latices and Knaster-Tarski theorem. Lecture notes.
Aug. 16, 18: Introduction to abstract interpretation. Lecture notes.
Aug. 21, 23, 28: Correctness of abstract interpretation. Associated lecture notes.
Aug. 30, Sep. 4, 6: Kildall's algorithm to compute least solution of data-flow equations. Associated lecture notes.
Sep. 11, 13, 18: Call strings approach to inter-procedural analysis.
Sep. 22, 25, Oct. 9: Functional approach to inter-procedural analysis.
Oct. 11, 13, 16: Pointer analysis
Oct. 18, 23, 25: Floyd-Hoare logic
Oct. 30, Nov. 3, 6: PDGs and slicing
Nov. 8, 13, 15: Simply Typed Lambda Calculus
Nov. 20, 22: Polymorphic type systems

Motivation

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 program slicing.

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 assumed.

Syllabus

Abstract 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 logic.

Reading material

Notes on domains and fix-points prepared by Prof. Thomas Reps.
Alfred Tarski, A lattice-theoretic fixpoint theorem and its applications, Pacific J. Mathematics, 5, pages 285--309, 1955.
Gary A. Kildall, A unified approach to global program optimization. In POPL '73: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 194--206, New York, NY, USA, 1973. ACM Press.
Patrick Cousot and Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, In POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238--252, New York, NY, USA, 1977. ACM Press.
Anders Møller and Michael I. Schwartzbach's book on dataflow analysis.
Micha Sharir and Amir Pnueli: Two approaches to interprocedural data-flow analysis, in Program Flow Analysis, Ed. Muchnik and Jones (1981). A scan of this paper.
Tom Reps, Susan Horwitz, Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability. (This is the IDFS paper.)
Lectures slides from Cornell University on Hoare logic.
Paper titled "ESP: Path-sensitive program verification in polynomial time" by Manuvir Das et al.
The paper "The semantics of slicing" by Thomas Reps and Wuu Yang.
S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs.
Jeanne Ferrante, Karl J Ottenstein, and Joe D Warren, The program dependence graph and its use in optimization.
Karl J Ottenstein and Linda M Ottenstein, The program dependence graph in a software development environment.
Notes on lambda calculus prepared by Prof. Thomas Reps.
Slides on lambda calculus: Rewrite-based term languages.
Benjamin C. Pierce, "Types and Programming Languages". Relevant chapters: Chapters 1-4 (preliminaries), 5 and 6 (basics of lambda calculus), and 8-9 (simple type systems, including simply typed lambda calculus).
Reading material on simple type inference: Simple type systems. Slides 1-16 are about a very simple type system (which we did not cover in class), whereas slides 17-27 are about simply typed lambda calculus.
L. Damas and R. Milner, Principal type-schemes for functional programs. In POPL '82, pages 207--212. This is our primary reference for polymorphic type inference.
There are two typographic errors in this paper:
- In Algorithm W, page 5, in item (ii), the first "let" should be W(A,e₁) = (S₁, τ₁).
- In item (iv) the first "let" should be W(A,e₁) = (S₁, τ₁).
Peter Hancock, Polymorphic type checking, and a type checker, Chapters 8 and 9 in Simon Peyton-Jones, "The Implementation of Functional Programming Languages", Prentice-Hall, New York. This is a secondary reference for polymorphic type inference. It gives more intuition and examples than the Damas-Milner paper. Covers unification (in Chap. 9).
Nielson, Nielson, and Hankin, "Principles of Program Analysis", Springer-Verlag. This is also a secondary reference for polymorphic type inference. The relevant sections are 5, 5.1, 5.1.1, 5.3, and 5.3.1. They cover unification quite clearly. You can read sections 5.1.2, 5.2, 5.3.2, 5.3.3, and 5.3.4 for extra information.