Lab for Automated Reasoning and Analysis LARA


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]
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$:
 ++++| ++++|
     sp^\#(a,r) = \alpha(sp(\gamma(a),​r)     sp^\#(a,r) = \alpha(sp(\gamma(a),​r)
 ++++ ++++
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