Differences

This shows you the differences between two versions of the page.

--- sav07_lecture_21 [2007/06/05 11:58]
vkuncak
+++ sav07_lecture_21 [2009/05/27 10:26]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Lecture 21: More on interprocedural analysis ======
-(Continuation of [[SAV07 Lecture 20]].)
+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) ===
   * Product construction based on push down automata and context-free grammar equivalence
+    * intersection of regular and context-free language is context-free
   * [[Reachable pushdown configurations are regular]]
+Reference:
+  * [[http://www.liafa.jussieu.fr/~abou/BEM97.ps.gz|Reachability Analysis of Pushdown Automata: Application to Model Checking]]
 === Non-regular properties using visibly pushdown languages ===
- * [[Visibly pushdown languages]]
+  * [[Visibly pushdown languages]]
-=== Two basic methods for inferring contracts ===
+Reference:
+ * [[http://www.cis.upenn.edu/~alur/Stoc04.pdf|Visibly pushdown languages]]
+=== Two basic methods for inferring contracts using Abstract Interpretation ===
   * approximate the set of (stack, state) pairs - based on small step semantics
@@ Line 25: / Line 34: @@
   * distributive functions and supergraph
   * checking context-free graph reachability
+  * [[http://doi.acm.org/10.1145/199448.199462|Precise interprocedural dataflow analysis via graph reachability]]
+  * [[http://research.microsoft.com/~maf/Papers/popl01.pdf|Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-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.
-=== References ===
+Reference:
+  * [[http://suif.stanford.edu/papers/wilson95.ps|Efficient Context-Sensitive Pointer Analysis for C Programs]]
+  * {{salcianu-phd.pdf|Sophisticated Pointer and Escape Analysis with Procedure Summaries}} (Alex Salcianu PhD thesis)
+=== 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.
   * {{knoop92interprocedural.pdf|The interprocedural coincidence theorem}}
   * F. Nielson, H. R. Nielson, C. Hankin: Principles of program analysis, 2005. Chapter 2.5.
-  * [[http://www.liafa.jussieu.fr/~abou/BEM97.ps.gz|Reachability Analysis of Pushdown Automata: Application to Model Checking]]
-  * [[http://doi.acm.org/10.1145/199448.199462|Precise interprocedural dataflow analysis via graph reachability]]
-  * [[http://research.microsoft.com/~maf/Papers/popl01.pdf|Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability]]
-  * [[http://www.cis.upenn.edu/~alur/Stoc04.pdf|Visibly pushdown languages]]
-  * [[http://suif.stanford.edu/papers/wilson95.ps|Efficient Context-Sensitive Pointer Analysis for C Programs]]