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:galois_connection_on_lattices [2008/05/07 23:45]
giuliano
sav08:galois_connection_on_lattices [2015/04/21 17:30] (current)
Line 34: Line 34:
 Define $sp^\#$ using $\alpha$ and $\gamma$: Define $sp^\#$ using $\alpha$ and $\gamma$:
 ++++| ++++|
-\[+\begin{equation*}
     sp^\#(a,r) = \alpha(sp(\gamma(a),​r)     sp^\#(a,r) = \alpha(sp(\gamma(a),​r)
-\]+\end{equation*}
 ++++ ++++
  
Line 46: Line 46:
  
 The most precise $sp^{\#}$ is called "best abstract transformer"​. The most precise $sp^{\#}$ is called "best abstract transformer"​.
 +
 +If $\alpha(\gamma(a)) = a$, then $sp^{\#}$ defined using $\alpha$ and $\gamma$ is the most precise one (given the abstract domain and particular blocks in the control-flow graph).
  
 
sav08/galois_connection_on_lattices.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice