• English only

# Lab for Automated Reasoning and Analysis 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:

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