LARA

Using Galois Connection

Terminology:

  • $C$ - concrete domain
  • $A$ - abstract domain
  • $\gamma$ - concretization function
  • $\alpha$ - abstraction function
  • $sp$ - (the usual) strongest postcondition (or just “strongest post”)
  • $sp^{\#}$ - abstract post, abstract transformer (transforms one abstract element into another)

Abstraction function for sign analysis.

Define $sp^\#$ using $\alpha$ and $\gamma$:

Best Abstract Transformer

$sp^{\#}$ can in general be arbitrarily imprecise while preserving correctness.

Given $\gamma$, we would like $sp^{\#}$ to be as precise as possible while being correct.

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).