# Powerset of Conjunctions of Predicates

Given the set of predicates , the domain are sets of sets of predicates.

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 program points, what is

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

Example: with

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 .

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

Relationship to abstract reachability tree.