# LARA

### Galois Connection

Galois connection is defined by two monotonic functions and between partial orders on and on , such that for all and (intuitively, the condition means that is approximated by ).

Lemma: The condition holds iff the conjunction of these two conditions: holds for all and .

Lemma: Let and satisfy the condition of Galois connection. Then the following three conditions are equivalent:

• for all • is a surjective function
• is an injective function

## Using Galois Connection

Terminology:

• - concrete domain
• - abstract domain
• - concretization function
• - abstraction function
• - (the usual) strongest postcondition (or just “strongest post”), also called
• - abstract post, abstract transformer (transforms one abstract element into another)

Abstraction function for sign analysis.

Define using and :

## Best Abstract Transformer can in general be arbitrarily precise while preserving correctness.

Given , we would like to be as precise as possible while being correct.

The most precise is called “best abstract transformer”.

If , then defined using and is the most precise one (given the abstract domain and particular blocks in the control-flow graph).