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
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
With such large domain, widening is even more important.
A natural widening is to go back to non-power domain element:
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.