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
γ	U+03B3	Gamma	Concretization
P	—	Predicates	Abstraction basis
𝔹ⁿ	—	Boolean	Abstract domain
→#	—	Abstract	Abstract transition

Metatheory. Sound abstraction. Galois connection. Completeness via refinement. Termination not guaranteed. Finite abstract state space.

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

Limitations. Predicate discovery hard. Exponential in predicates. CEGAR may not terminate. Interprocedural challenging.