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.

 \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) \}

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:

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

P_1 &\equiv& 0 < x \\
P_2 &\equiv& 0 < y \\
P_3 &\equiv& x <= 0 \\
P_4 &\equiv& y <= 0 \\

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.