CS638 : Program Analysis
(PG Elective for the II senester)

Uday Khedker

1. Background.

   This course is an outcome of a UG elective (CS 412: Introduction to Program Analysis), a PG elective (CS:614 Advanced Compilers) which I have taught in past two years and my research (in collaboration with my colleagues) in past three years. Thus, this is a fairly new and fresh course.

2. Overall Plan.

   The course begins with the mathematical foundations of program analysis and then concentrates on advanced applications of data flow analysis. The advances are in terms of data flow properties which cannot be represented using bit vectors which is the usual model discussed even in advanced courses.

3. Course Contents.
   1. Mathematical Foundations of Program Analysis Lattices: partial orders and approximations, bounded lattices, complete lattices.
      Function spaces: monotonicity, distributivity, separability, boundedness.
      Fixed Point Computations: least fixed point and induction, greatest fixed point and co-induction.

      Abstract interpretation: concretisation and abstraction functions, Galois connection.

   2. Alias analysis of heap data

      Type of alias information: Context sentitive/insensitive, flow sensitive.insensitive, may/must aliases.
      Representations of heap properties: shape graphs, alias graphs, storage shape graphs, k-limiting, compact representations, access graphs.
      Data flow analysis for aliases.

   3. Liveness analysis of heap data

      Shape graphs and heap safety automaton based approach.

   4. Static type inferencing of flow sensitive polymorphic types.

      Type inferencing for validation and type inferencing for optimization.

      Data flow analysis for monomorphic languages. Extensions for polymorphic types, type graphs and operations.

   5. Interprocedural data flow analysis

      Context sensitive/insensitive analysis. Functional approach. Call strings approach. Call strings graphs. Call strings approach for k-bounded problems.

4. Reading Material.

   There is no particular book which can be used as a text book. The course is based on research papers and selected book chapters listed in the reference list.

5. Prerequisites. First course in compiler construction.

6. Other Faculty Interested in This Area.

   Prof. A. Sanyal, Prof. S. Biswas Prof. D. M. Dhamdhere