CSE 590 MD: Program Analysis

    
 

Instructor: Manuvir Das

    
 

Reading List

Spring 2001
 
 
  1. Overview - books that are handy references

    [ASU 88] A. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1988.

    [MJ 81] S. Muchnick and N. D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice Hall, 1981.

    [NN 99] F. Neilson, H. R. Neilson, and C. Hankin. Principles of Program Analysis. Springer, 1999.

    [FH 88] A. Field and P. Harrison. Functional Programming. Addison-Wesley, 1988.

    [AH 97] S. Abramsky and C. Hankin, editors. Abstract Interpretation of Declarative Languages    . Ellis Horwood, 1987.

    [Gri 87] D. Gries. The Science of Programming. Springer-Verlag, 1987.
  2. Flow-sensitive analysis
    Context-sensitive Dataflow:

    Basic Theory: [SP 81] M. Sharir and A. Pnueli. Two approaches to interprocedural dataflow analysis. In [MJ 81], pages 189-234.

    Efficient Algorithm: [RHS 95] T. Reps, S. Horwitz, and M. Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. In Conference Record of the Twenty-Second ACM Symposium on Principles of Programming Languages, 1995.

    Further readings: provided by Erik Ruf.

    Program Slicing:

    [HRB 90]     S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems Vol 12, 1 (January 1990), pages 26-60.

  3. Abstract interpretation
    Basic Theory: [CC 77] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977.

  4. Flow-insensitive analysis

    Polymorphic Type Inference:

    Introduction: [FH 88a] Chapter 7 from [FH 88].

    Algorithm W: [Mil 78] R. Milner. A Theory of Type Polymorphism in Programming. In Journal of Computer and System Sciences, 17, pp. 348-375.

    Analysis via Non-standard Type Inference:

    Context-insensitive, non-directional: [Ste 96] B. Steensgaard. Points-to Analysis in Almost Linear Time. In Conference Record of the Twenty-Third ACM Symposium on Principles of Programming Languages, 1996.

    [Note] Note on Steensgaard's Analysis.

    Context-sensitive: [FRD 00] M. Fahndrich, J. Rehof, and M. Das. Scalable Context-Sensitive Flow Analysis Using Instantiation Constraints. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2000.

    Further readings on polymorphic type inference: provided by Jakob Rehof

    Directional: [Aik 99] A. Aiken. Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming, 35(1999):79-111.

    Further readings on set constraints    : provided by Manuel Fahndrich

    Effect systems: [TT 94] M. Tofte and J. Talpin. Implementation of the Typed Call-by-Value Lambda-calculus using a Stack of Regions. In Conference Record of the Twenty-First ACM Symposium on Principles of Programming Languages, 1994.

    Adding flow-sensitivity:

    SSA:     [CFR+ 89] R. Cytron, F. Ferrante, B. Rosen, M. Wegman, and F. Zadeck. An efficient method for computing static single assignment form. In Conference Record of the Sixteenth ACM Symposium on Principles of Programming Languages, 1989.

    Efficient SSA: [SG 95] V. Sreedhar and G. Gao. A linear time algorithm for placing phi nodes. In Conference Record of the 22nd ACM Symposium on Principles of Programming Languages, 1995.

  5. Path-sensitive analysis

    Path simulation:

    Practical path exploration: [BPS 00] W. Bush, J. Pincus, and D. Sielaff. A Static Analyzer for Finding Dynamic Programming Errors. Software - Practice and Experience 30(7): pp. 775-802.

    Decision procedures:

    Uninterpreted functions: [NO 80] G. Nelson and D. Oppen. Fast Decision Procedures Based on Congruence Closure. JACM, Vol 27, No 2, April 1980, pp. 356-364.

    Adding theories: [NO 79] G. Nelson and D. Oppen. Simplification by Cooperating Decision Procedures. ACM TOPLAS, Vol 1, No 2, Oct 1979, pp. 245-257.

    Model checking:

    Overview: [CGL 93] E.     Clarke, O. Grumberg, and D. Long. Verification Tools for Finite-State Concurrent Systems. LNCS 803, Proceedings of REX school/symposium on A decade of concurrency: reflections and perspectives, Noordwijkerhout, The Netherlands, June 1993.

    Further readings on model checking    : provided by Sriram Rajamani.

    Verification:

    WP and SP: [Gri 87a] Chapters 6-11 from [Gri 87].
  6. Other  analysis techniques

    Pointer analysis:

    Fast subtyping algorithm: [Das 00] M. Das, Unification-based Pointer Analysis with Directional Assignments. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2000.

    Fast context-sensitive algorithm with subtyping: [DLFR 01] M. Das, B. Liblit, M. Fahndrich, and J. Rehof. Estimating the Impact of Scalable Pointer Analysis on Optimization. To appear in SAS 2001.

    Call graph analysis in OO programs:

    General Framework: [GC 01] D. Grove and C. Chambers, A Unifying Framework for and Assessment of Call Graph Construction Algorithms. To appear in ACM TOPLAS. (Contact Craig Chambers for a draft version.)
  7. Dynamic analysis

    Program profiling:

    Method for improving dataflow:     [AL 98] G. Ammons and J. Larus, Improving data-flow analysis with path profiles. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 1998.

    Continuous profiling:     [ABD+ 97] J. Anderson, L. Berc, J. Dean, S. Ghemawat, M. Henzinger, S. Leung, R. Sites, M. Vandevoorde, C. Waldspurger, and W. Weihl, Continuous Profiling: Where Have All the Cycles Gone? In Proceedings of the 16th ACM Symposium on Operating Systems Principles, October 1997.

  8. Examples of analysis projects

    Vault:     [DF 01] R. Deline and M. Fahndrich. Enforcing High-Level Protocols in Low-Level Software. To be presented at PLDI 01.

    SLAM: [BR 01] T. Ball and S. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces. SPIN 2001.

    ESP: [Das 01] M. Das, ESP: Error Detection via Scalable Program Analysis.     (Contact Manuvir Das for a draft version.)
Additional info:
Introduction
 Information
 Topics
Lecture Schedule
 Lecture Notes
 Reading List
 Homework


Email Manuvir
 
     
 

CSE 590MD © 2001, Department of Computer Science and Engineering, University of Washington.