Statement	Inclusion Constraint
a = b	PointsToSet(b) ⊆ PointsToSet(a)
a = &b	b ∈ PointsToSet(a)
a = *b	∀c ∈ PointsToSet(b): PointsToSet(c) ⊆ PointsToSet(a)
*a = b	∀c ∈ PointsToSet(a): PointsToSet(b) ⊆ PointsToSet(c)

Inputs	Description
A	a set of n pointers
S	a set of m statements

m ≤ 4*n^2 unique statements

Output	Description
Exhaustive	Return PointsToSet(a) for all pointers a ∈ A
On-demand	Return if b ∈ PointsToSet(a) for a specific pair a, b ∈ A

---

1. [POPL 2021] The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis