Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:abstract_interpretation_recipe [2008/05/08 12:41]
vkuncak
sav08:abstract_interpretation_recipe [2015/04/21 17:30] (current)
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$
  
 
sav08/abstract_interpretation_recipe.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice