Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_lecture_21 [2009/05/27 01:48] vkuncak |
sav07_lecture_21 [2009/05/27 10:26] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Lecture 21: More on interprocedural analysis ====== | ====== 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) === | === 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 | * 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]] | * [[Reachable pushdown configurations are regular]] | ||
| Line 11: | Line 16: | ||
| === Non-regular properties using visibly pushdown languages === | === Non-regular properties using visibly pushdown languages === | ||
| - | * [[Visibly pushdown languages]] | + | * [[Visibly pushdown languages]] |
| Reference: | Reference: | ||
| * [[http://www.cis.upenn.edu/~alur/Stoc04.pdf|Visibly pushdown languages]] | * [[http://www.cis.upenn.edu/~alur/Stoc04.pdf|Visibly pushdown languages]] | ||
| - | === Two basic methods for inferring contracts === | + | === Two basic methods for inferring contracts using Abstract Interpretation === |
| * approximate the set of (stack, state) pairs - based on small step semantics | * approximate the set of (stack, state) pairs - based on small step semantics | ||