Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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