Powerset of Conjunctions of Predicates

We now apply Powerdomains for Finite Domains to Abstract Interpretation with Conjunctions of Predicates.

Given the set of predicates ${\cal P}$ , the domain are sets of sets of predicates.

$\begin{equation*} \begin{array}{l} \gamma(\{\{P_1,P_2\}, \{P_0,P_3\}\}) = \\ \gamma(\{P_1,P_2\}) \cup \gamma(\{P_0,P_3\}) = \\ \{(x,y).\ P_1(x,y) \land P_2(x,y))\} \cup \{(x,y).\ P_0(x,y) \land P_3(x,y))\} = \\ \{(x,y). ((P_1 \land P_2) \lor (P_0 \land P_3))(x,y) \} \end{array} \end{equation*}$

Result are disjunctions of conjunctions of predicates i.e. arbitrary boolean combinations of predicates.

This is the domain used in predicate abstraction techniques.

Even stronger domains are obtained when we allow quantified formulas. See:

Symbolic Shape Analysis, PhD dissertation by Thomas Wies

Given a fixed number of predicates and $p$ program points, what is

the number of elements of this powerset lattice
height of this powerset lattice

Example: ${\cal P} = \{ P_1, P_2, P_3, P_4 \}$ with

$\begin{equation*} \begin{array}{rcl} P_1 &\equiv& 0 < x \\ P_2 &\equiv& 0 < y \\ P_3 &\equiv& x <= 0 \\ P_4 &\equiv& y <= 0 \\ \end{array} \end{equation*}$

Consider this program where the initial values of x and y are arbitrary. Compute abstraction using conjunctions of predicates, as well as disjunction of conjunctions of predicates, if we have predicates $\{ x > 0, x <= 0, y > 0, y <= 0 \}$ .

if (x > 0) {
  y = 1
} else {
  y = -1
}

Relationship to abstract reachability tree.