Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_lecture_9 [2007/04/19 11:20] vkuncak |
sav07_lecture_9 [2007/05/11 17:25] ghid.maatouk |
||
|---|---|---|---|
| Line 32: | Line 32: | ||
| \end{equation*} | \end{equation*} | ||
| where $a^1,\ldots,a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph). | where $a^1,\ldots,a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph). | ||
| + | |||
| Line 80: | Line 81: | ||
| * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml|Abstract interpretation]] | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml|Abstract interpretation]] | ||
| * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]] | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]] | ||
| + | |||
| + | ===Tarski's Fixpoint Theorem=== | ||
| === Widening === | === Widening === | ||
| Line 104: | Line 107: | ||
| === Narrowing === | === Narrowing === | ||
| - | Once we have reached above the fixpoint (using widening or anything else), we can always apply the fixpoint transformer and improve the precision of the results. | + | Once we have reached above the fixpoint (using widening or anything else), we can always apply the fixpoint operator $G$ and improve the precision of the results. |
| + | |||
| + | If this is too slow, we can stop at any point or use a narrowing operator, the result is sound. | ||
| + | |||
| + | Instead of using the fixpoint operator $G$, we can use any operator that leaves our current value above fixpoint. | ||
| - | If this is too slow, we can stop at any point or use a narrowing operator. | + | See Combination of Abstractions in ASTREE, Section 8.1, define $\Delta$ such that $\gamma(a) \cap \gamma(b) \subseteq \gamma(a \Delta b)$ |
| + | * example: take $\sqcap$ as $\Delta$, or even some improved version | ||
| === Reduced product === | === Reduced product === | ||