# LARA

## Using Galois Connection

Terminology:

• - concrete domain
• - abstract domain
• - concretization function
• - abstraction function
• - (the usual) strongest postcondition (or just “strongest post”)
• - 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 imprecise 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).