Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_9 [2007/04/19 10:53] vkuncak |
sav07_lecture_9 [2007/04/19 11:13] vkuncak |
||
---|---|---|---|
Line 100: | Line 100: | ||
* drawback: not monotonic (example), so more difficult to reason about | * drawback: not monotonic (example), so more difficult to reason about | ||
- | Often the operator is defined not just on the current fact $x$ but as a binary operator that takes $x$ and $G(x)$, denoted $x \nabla G(x)$, we require $x \sqcup y \sqsubseteq x \nabla y$. | + | Often the operator is defined not just on the current fact $x$ but as a binary operator that takes $x$ and $G(x)$, denoted $x \nabla G(x)$, with property $a \sqcup b \sqsubseteq a \nabla b$. |
=== Narrowing === | === Narrowing === | ||
Line 113: | Line 113: | ||
To obtain more precise results, we allow analyses to exchange information. | To obtain more precise results, we allow analyses to exchange information. | ||
+ | |||
+ | Reduced product: [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]], Section 10.1. | ||
+ | |||