Predicate Abstraction

Origin. Graf and Saïdi (1997). Abstract interpretation guided by predicates. Boolean programs from concrete programs. CEGAR loop. Foundation for SLAM, BLAST.

Models. Predicates abstract state to boolean combinations. Concrete state s maps to predicate valuation. Sound abstraction: preserves safety. Refinement adds predicates.

Formalism.

Predicates: P = {p₁, ..., pₙ} set of predicates over program state. Each pᵢ: State → Bool.

Abstract state: b = (b₁, ..., bₙ) ∈ 𝔹ⁿ bᵢ = pᵢ(s) for concrete state s.

Abstraction function: α(s) = (p₁(s), ..., pₙ(s)) α(S) = {α(s) | s ∈ S}

Concretization: γ(b) = {s | ∧ᵢ(bᵢ ↔ pᵢ(s))} States satisfying the abstract state.

Abstract transition: b →# b' iff ∃s ∈ γ(b), s' ∈ γ(b'). s → s'

Cartesian abstraction: Independent predicates. Abstract state: conjunction of literals.

Boolean abstraction: Full boolean combinations. More precise, more expensive.

CEGAR (CounterExample Guided Abstraction Refinement):

Start with coarse predicates
Model check abstract program
If safe: done
If spurious counterexample: refine predicates
Repeat

Weakest precondition: wp(x := e, p) = p[e/x] Derive new predicates via interpolation.

Symbols.

Symbol	Unicode	Name	Meaning
α	U+03B1	Alpha / Abstraction map	Sends a concrete state to its predicate valuation
γ	U+03B3	Gamma / Concretization map	Sends an abstract state to the states it denotes
P	—	Predicate set	{p₁, …, pₙ}, the basis of the abstraction
pᵢ	—	Predicate	A map State → Bool
b	—	Abstract state	The bit vector (b₁, …, bₙ)
𝔹	U+1D539	Double-struck capital B / Booleans	Value domain of a single predicate
ⁿ	U+207F	Superscript Latin small letter N	Exponent: 𝔹ⁿ, the abstract domain
→#	—	Abstract transition	Existential lifting of → through γ (arrow plus number sign)
→	U+2192	Rightwards arrow / Concrete step	Transition of the concrete program
∈	U+2208	Element of	Membership of a concrete state in γ(b)
∃	U+2203	There exists	Existential abstraction of the transition relation
∧	U+2227	Logical and	Conjunction over the predicates in γ(b)
↔	U+2194	Left right arrow / Biconditional	bᵢ ↔ pᵢ(s), agreement of bit and predicate
wp	—	Weakest precondition	Source of refinement predicates, wp(x := e, p) = p[e/x]
CEGAR	—	Refinement loop	Counterexample-guided abstraction refinement

Metatheory. Graf and Saïdi's 1997 construction is an abstract interpretation in the Cousot sense: α and γ form a Galois connection between the powerset of concrete states and 𝔹ⁿ, and the existentially lifted abstract transition over-approximates the concrete one, so soundness is by construction and no separate argument is needed. Preservation is one-directional in a way made precise by Clarke, Grumberg, and Long (1994): universal path properties proved of the abstraction hold of the program, while an abstract counterexample may be spurious. The abstract state space is 2ⁿ in the number of predicates, and computing the most precise abstract post-image requires exponentially many theorem-prover queries, which is why SLAM's Cartesian abstraction gives up precision for a linear number. CEGAR (Clarke, Grumberg, Jha, Lu, and Veith, 2000) closes the loop by mining new predicates from the infeasibility proof of a spurious counterexample — in the later systems by Craig interpolation (McMillan, lazy abstraction with interpolants, 2006). The result is a semi-algorithm: terminating on finite-state systems, and by Rice's theorem incapable of always terminating on the infinite-state ones it is aimed at.

Applies to. SLAM (Windows drivers). BLAST. Software model checking. Property verification. Security analysis.

Limitations. The abstraction is sound but not complete, and the gap is not repairable in general: no finite set of predicates need suffice, because the invariant a program requires may not be a Boolean combination of any finite set of atomic formulas drawn from its syntax — quantified invariants over arrays and unbounded heap structures are the standard witnesses. Refinement therefore has no termination guarantee; each spurious counterexample contributes at least one predicate, but the sequence may grow without bound, and Rice's theorem rules out any procedure that always halts with an answer. Cost is exponential in two places at once: 2ⁿ abstract states, and exponentially many solver queries for the most precise abstract post, so the abstractions actually used are deliberately imprecise and generate spurious counterexamples of their own. Only universal path properties transfer across the abstraction, so existential properties and hyperproperties are not preserved.