Lab for Automated Reasoning and Analysis LARA

Lecture 21: More on interprocedural analysis

The idea is to avoid having to specify contracts for all procedures

  • abstract interpretation for general case (precision depends on the example)
  • decidability results: no approximation, but works for restricted classes of programs (which can be obtained by abstract interpretation)

Analysis of regular properties of finite-state programs with stack (push down systems)

Reference:

Non-regular properties using visibly pushdown languages

Two basic methods for inferring contracts using Abstract Interpretation

  • approximate the set of (stack, state) pairs - based on small step semantics
    • call-string approach
    • representing stack as e.g. linked list (see this paper)
  • approximate the relation between initial and final state of procedure - based on big step semantics
    • add procedure entry variables, then approximate (consider e.g. linear constraints)
    • functional approach: map entry data flow facts to exit data flow facts

Analysis based on graph reachability

Summaries for pointer analysis

Computations on heap can give different result depending on whether in precondition certain references refer to same objects or not. Procedure specifications are therefore important for such programs and automatically inferring them is challenging.

Reference:

General References

  • M. Sharir, and A. Pnueli. Two Approaches to Inter-Procedural Data-Flow Analysis. In Jones and Muchnik, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.
  • F. Nielson, H. R. Nielson, C. Hankin: Principles of program analysis, 2005. Chapter 2.5.
 
sav07_lecture_21.txt · Last modified: 2009/05/27 10:26 by vkuncak