# Differences

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

 sav08:abstract_interpretation_recipe [2008/05/08 12:41]vkuncak sav08:abstract_interpretation_recipe [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/20 12:14 vkuncak 2008/05/08 12:41 vkuncak 2008/05/08 12:40 vkuncak 2008/05/08 12:39 vkuncak 2008/05/08 12:38 vkuncak 2008/05/08 12:38 vkuncak 2008/05/08 12:24 vkuncak 2008/05/08 12:24 vkuncak 2008/05/08 12:23 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:21 vkuncak 2008/05/08 12:19 vkuncak 2008/05/08 12:19 vkuncak 2008/05/08 12:16 vkuncak 2008/05/08 12:15 vkuncak 2008/05/07 23:37 giuliano 2008/05/07 08:43 vkuncak created Next revision Previous revision 2008/05/20 12:14 vkuncak 2008/05/08 12:41 vkuncak 2008/05/08 12:40 vkuncak 2008/05/08 12:39 vkuncak 2008/05/08 12:38 vkuncak 2008/05/08 12:38 vkuncak 2008/05/08 12:24 vkuncak 2008/05/08 12:24 vkuncak 2008/05/08 12:23 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:22 vkuncak 2008/05/08 12:21 vkuncak 2008/05/08 12:19 vkuncak 2008/05/08 12:19 vkuncak 2008/05/08 12:16 vkuncak 2008/05/08 12:15 vkuncak 2008/05/07 23:37 giuliano 2008/05/07 08:43 vkuncak created Line 17: Line 17: (for example, by defining function $\alpha$ so that $(\alpha,​\gamma)$ becomes a [[Galois Connection on Lattices]]) (for example, by defining function $\alpha$ so that $(\alpha,​\gamma)$ becomes a [[Galois Connection on Lattices]]) * extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$) * extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$) - $+ \begin{equation*} - ​F^{\#​}(g^{\#​})(p_2) = g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} sp^{\#​}(g^{\#​}(p_1),r(p_1,p_2)) + ​F^{\#​}(g^{\#​})(p') = g^{\#}(p') \sqcup \bigsqcup_{(p,p') \in E} sp^{\#​}(g^{\#​}(p),r(p,p')) -$ + \end{equation*} which is analogous to [[Collecting Semantics]] which is analogous to [[Collecting Semantics]] * compute $g^{\#}_* = lfp(F^\#)$ (this is easier than computing collecting semantics because lattice $A^n$ is simpler than $C^n$): * compute $g^{\#}_* = lfp(F^\#)$ (this is easier than computing collecting semantics because lattice $A^n$ is simpler than $C^n$): - $+ \begin{equation*} ​g^{\#​}_* = \bigsqcup_{n \ge 0} (F^{\#​})^{n}(\bot^{\#​}) ​g^{\#​}_* = \bigsqcup_{n \ge 0} (F^{\#​})^{n}(\bot^{\#​}) -$ + \end{equation*} where $\bot^{\#​}(p) = \bot_A$ for all $p \in V$ where $\bot^{\#​}(p) = \bot_A$ for all $p \in V$