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:54] vkuncak |
sav07_lecture_9 [2007/04/19 11:18] vkuncak |
||
|---|---|---|---|
| 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. | ||
| + | |||
| + | Key point: define $\sigma : A_1 \times A_2 \to A_1 \times A_2$ by | ||
| + | \begin{equation*} | ||
| + | \sigma(a_1,a_2) = \sqcap \{ (a_1',a_2') \mid \gamma(a_1') \cap \gamma(a_2') = \gamma(a_1) \cap \gamma(a_2) \} | ||
| + | \end{equation*} | ||
| + | The function $\sigma$ improves the precision of the element of the lattice without changing its meaning. Subsequent computations with these values then give more precise results. | ||
| + | |||