Madhavan Mukund

Program Analysis

Jan-April, 2014

Textbook

• Principles Of Program Analysis
  by Flemming Nielson, Hanne Riis Nielson, Chris Hankin
  (referred to as NNH below)

Supplementary Reading Material

• Micha Sharir and Amir Pnueli: Two Approaches to Inter-Procedural Data-Flow Analysis. In Neil Jones and Steven Muchnik, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981

• Thomas Reps: Program Analysis via Graph Reachability

• Lars Ole Andersen: Pointer Analysis, Chapter 4 of his PhD Thesis, Program Analysis and Specialization for the C Programming Language,1994.

• Bjarne Steensgaard: Points-to Analysis in Almost Linear Time, POPL 1996

• Derek Rayside: Points-to Analysis (notes), MIT, 2005

• Aaron R. Bradley and Zohar Manna: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.

Assignments and Projects

• Assignment 1, 5 March 2014, due 21 March 2014

• Project 1, 5 March 2014, due 4 April 2014

• Assignment 2, 13 April 2014, due 25 April 2014

Lectures

• Lecture 1, Thu 16 Jan 2014: Introduction to the course

  • Examples of compiler optimization, dataflow analysis, abstract interpretation (NNH Chapter 1.1–1.3, 1.5)

• Lecture 2, Tue 21 Jan 2014: Some standard dataflow analyses

  • Building a flow graph, examples of forward/backward and maximal/minimal solutions, monotone and distributive frameworks (NNH Chapter 2.1.1–2.1.4, 2.3.1–2.3.2)

• Lecture 3, Thu 23 Jan 2014: Derived analysis, non-distributivity, equation solving

  • ud and du chains, non-distributivity of constant propagation, MFP vs MOP, undecidability of MOP (NNH Chapter 2.1.5, 2.3.3, 2.4)

• Lecture 4, Tue 28 Jan 2014: Structural operational semantics, Interprocedural analysis

  • Structural operational semantics for while programs, proving formal correctness for a specific type of analysis (NNH Chapter 2.2)
  • Flow graphs for programs with recursive procedures, valid paths, making context explicit, call strings as context (NNH Chapter 2.5, 2.5.2–2.5.4)

• Lecture 5, Tue 04 Feb 2014: Shape Analysis

  • Adding pointers to the language, operational semantics, shape graphs (NNH Chapter 2.6)

• Lecture 6, Thu 06 Feb 2014: Shape Analysis

  • Forward analysis using shape graphs (NNH Chapter 2.6)

• Lecture 7, Tue 11 Feb 2014: Interprocedural Analysis, functional approach

  Sharir-Pnueli's functional approach to interprocedural analysis

• Lecture 8, Thu 13 Feb 2014: Interprocedural Analysis, functional approach vs call strings

  Sharir-Pnueli's interprocedural analysis

  • Functional approach: computing the functions incrementally as tables
  • Call strings as context

• Lecture 9, Tue 18 Feb 2014: Interprocedural Analysis via CFL reachability

  • Paper by Thomas Reps, listed above under Supplementary Reading.

• Lecture 10, Tue 04 Mar 2014: Introduction to abstract interpretation

  • Correctness relations and representation functions (NNH Chapter 4.1)
  • Approximation of fixed points: Widening and narrowing (NNH Chapter 4.2)

• Lecture 11, Tue 11 Mar 2014: Galois connections

  • Galois connections and adjunctions, extraction functions, Galois insertions, reduction operators (NNH Chapter 4.3)

• Lecture 12, Thu 13 Mar 2014: Galois connections (continued)

  • Systematic design of Galois connections: component-wise and other combinations (NNH Chapter 4.4)
  • Induced operations: inducing along the abstraction function, applications to data flow analysis, inducing along the concretization function (NNH Chapter 4.5)

• Lecture 13, Thu 20 Mar 2014: Pointer Analysis

  • Approaches due to Andersen and Steensgaard (see Supplementary Material for papers by Andersen and Steensgaard and notes by Rayside.)

• Lecture 14, Tue 25 Mar 2014: Software Verification

  • Counter Example Guided Abstraction Refinement (CEGAR) – Introduction to SLAM
  • Hoare logic and weakest preconditions

• Lecture 15, Thu 27 Mar 2014: Software Verification (continued)

  • SLAM internals:
    • c2bp: constructing a boolean abstraction of a C program
    • bebop: model-checking boolean program using interprocedural analysis

• Lecture 16, Tue 08 Apr 2014: Software Verification (continued)

  • Abstraction refinement:
    • Extracting new predicates from spurious counterexamples
    • Interpolants

• Lecture 17, Tue 15 Apr 2014: Invariant generation

  • Abstract interpretation based invariant generation
    (Bradley and Manna, Chapter 12.1)

• Lecture 18, Thu 17 Apr 2014: Invariant generation (continued)

  • Interval analysis (Bradley and Manna, Chapter 12.2)
  • Affine assertions: Karr's Analysis (Bradley and Manna, Chapter 12.3)