# Powerdomains

Let be a lattice.

Define with .

The lattice is exponentially larger, and it can be much more precise.

Example: applying powerdomain to interval lattice means that we can represent every possible set of states from concrete execution, because each element can be represented by abstract state with exact intervals.

Given , define by

We define

and there is no approximation in , that is,

The abstraction function can be defined for each state, for , we have , so

Example: Abstracting set by interval gives

Abstracting it by powerset of interval gives

Also, we can define

Example:

With such large domain, widening is even more important.

A natural widening is to go back to non-power domain element:

Example:

We can also apply the standard interval widening (with “jumps”) on top of this.

So, we can get precision or efficiency, depending on the use of widening.