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:chaotic_iteration_in_abstract_interpretation [2008/05/20 18:50]
vkuncak
sav08:chaotic_iteration_in_abstract_interpretation [2015/04/21 17:30] (current)
Line 1: Line 1:
-====== Chaotic Iteration in Abstract Interpretation ======+====== Chaotic Iteration in Abstract Interpretation: How to compute the fixpoint? ​======
  
 In [[Abstract Interpretation Recipe]], note that if the set of program points is $p'​_1,​\ldots,​p'​_n$,​ then we are solving the system of eqautions in $n$ variables $g_1,​\ldots,​g_n$ In [[Abstract Interpretation Recipe]], note that if the set of program points is $p'​_1,​\ldots,​p'​_n$,​ then we are solving the system of eqautions in $n$ variables $g_1,​\ldots,​g_n$
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
     g_1 = H_1(g_1,​\ldots,​g_n) \\     g_1 = H_1(g_1,​\ldots,​g_n) \\
Line 10: Line 10:
     g_n = H_n(g_1,​\ldots,​g_n) \\     g_n = H_n(g_1,​\ldots,​g_n) \\
 \end{array} \end{array}
-\]+\end{equation*}
 where  where 
-\[+\begin{equation*}
    H_i = g_i \sqcup \bigsqcup_{(p_j,​p_i) \in E} sp^{\#​}(g_j,​r(p_j,​p_i))    H_i = g_i \sqcup \bigsqcup_{(p_j,​p_i) \in E} sp^{\#​}(g_j,​r(p_j,​p_i))
-\]+\end{equation*}
 The approach given in [[Abstract Interpretation Recipe]] computes in iteration $k$ values $g^k_i$ by applying all equations in parallel to previous values: The approach given in [[Abstract Interpretation Recipe]] computes in iteration $k$ values $g^k_i$ by applying all equations in parallel to previous values:
-\[+\begin{equation*}
 \begin{array}{ll} \begin{array}{ll}
     g^{k+1}_1 = H_1(g^k_1,​\ldots,​g^k_n) \\     g^{k+1}_1 = H_1(g^k_1,​\ldots,​g^k_n) \\
Line 24: Line 24:
     g^{k+1}_n = H_n(g^k_1,​\ldots,​g^k_n) \\     g^{k+1}_n = H_n(g^k_1,​\ldots,​g^k_n) \\
 \end{array} \end{array}
-\]+\end{equation*}
  
 What happens if we update values one-by-one? ​ Say in one iteration we update $i$-th value, keeping the rest same: What happens if we update values one-by-one? ​ Say in one iteration we update $i$-th value, keeping the rest same:
-\[+\begin{equation*}
 \begin{array}{ll} \begin{array}{ll}
     g^{k+1}_i = H_i(g^k_1,​\ldots,​g^k_n) ​ \\     g^{k+1}_i = H_i(g^k_1,​\ldots,​g^k_n) ​ \\
Line 33: Line 33:
     g^{k+1}_j = g^k_j, \mbox{ for } j \neq i      g^{k+1}_j = g^k_j, \mbox{ for } j \neq i 
 \end{array} \end{array}
-\]+\end{equation*}
 here we require that the new value $H_i(g^k_1,​\ldots,​g^k_n)$ differs from the old one $g^k_i$. ​ An iteration where at each step we select some equation $i$ (arbitrarily) is called //chaotic iteration//​. ​ It is abstract representation of different iteration strategies. here we require that the new value $H_i(g^k_1,​\ldots,​g^k_n)$ differs from the old one $g^k_i$. ​ An iteration where at each step we select some equation $i$ (arbitrarily) is called //chaotic iteration//​. ​ It is abstract representation of different iteration strategies.
    
 
sav08/chaotic_iteration_in_abstract_interpretation.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice