Program Analysis and Verification

E0 227 Program Analysis and Verification

August-December 2011, 3:30pm-5:00pm Tue, 2pm-3:30pm Fri, CSA Lecture Hall (Room 117)

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

Teaching assistants: Amogh Margoor and Aravind Acharya (both II Year MSc Engg.)

Assignments

Assignment 1, on abstract interpretation. Posted Sep. 2nd. Due Sep. 12th. Will not be accepted after Sep. 17th. Some clarifications.
Assignment 2, on lattices and Kildall's algorithm. Posted Sep. 16th. Due Sep. 25th. Will not be accepted after the midsem exam on Sep. 30th.
Assignment 3, on inter-procedural analysis, the ESP paper, and points-to analysis. Posted Oct. 26th. Due Nov. 7th. Will not be accepted after Nov. 11th.
Assignment 4, on type systems and Hoare logic. Posted Nov. 20th. Due Dec. 2nd 9am. No delays permitted.

Lecture slides

Aug. 2: Overview of all SE courses, Overview of PAV and FMSE
Aug. 4: Introduction
Aug. 9, 16: Lattices
Aug. 23, 25: Abstract Interpretation
Aug. 26, 30: Correctness of Abstract Interpretation
Sep. 2, 6: Kildall's algorithm.
Sep. 9, 13: Interprocedural analysis using call strings
Sep. 16, 20: Functional approach to inter-procedural analysis.
Sep. 23, 27: Interprocedural analysis of IDFS problems.
Sep. 30: Midsem exam.
Oct. 4, 7: Discussion of paper on path-sensitive data-flow analysis. A few lecture slides explaining some of the concepts in the paper.
Oct. 11: Pointer analyis, part 1: pptx (has better formatting and animation), pdf
Oct. 14: Pointer analyis, part 2: pptx (has better formatting and animation), pdf
Oct. 18: Review of midsem exam. Programming project announcement.
Oct. 21: Brief introduction to lambda calculus.
Oct. 25, Nov. 4: Hoare logic.
Nov. 8, 11: Simply Typed Lambda Calculus.
Nov. 15, 16: Polymorphic type systems.
Nov. 18, 22: Algorithm for polymorphic type inference.
Nov. 25, 29: Paper on using a type system to prove deadlock- and race-freedom in concurrent programs. We are focusing only on Sections 1-3.
Dec. 8th, 2pm-5pm: Final exam.

Programming project

Here is the project's description.

This tar ball contains the Soot JAR file, a presentation about Soot (including a link to a detailed tutorial), and skeleton source for you to use (with JavaDoc generated from it).

The project will have an initial demo on November 22/23, by which time you ought to have completed your implementation, and be able to run it on all the test cases we have provided. We will then have a final demo on November 28th when you will demonstrate the changes you made based on the feedback we gave you during your initial demo. These dates are strict, with no delays permitted.

Here are a set of test cases for you to use (we will have an additional set of test cases for evaluation).

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 a program, properties that programmers wish to prove about programs, and the theory behind foundational program-analysis techniques such as abstract interpretation, type inference, and theorem proving.

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

Denotational and operational semantics of programs. 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 and polymorphic type systems, Hindley-Milner's type inference algorithm for functional programs. Pointer analysis of imperative programs. 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.
Micha Sharir and Amir Pnueli: Two approaches to interprocedural data-flow analysis, in Program Flow Analysis, Ed. Muchnik and Jones (1981). (Other three interprocedural dataflow analysis approaches.)
Tom Reps, Susan Horwitz, Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability.
Notes on lambda calculus prepared by Prof. Thomas Reps.
Slides on lambda calculus: Rewrite-based term languages.
Lectures slides from Cornell University on Hoare logic.
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.