Module abstraction 

Predicate Abstraction with CEGAR Refinement

Predicate abstraction reduces an infinite-state system to a finite-state boolean system over abstract predicate variables. Each concrete predicate (e.g., x >= 0) becomes an abstract boolean. The abstract transition encodes how predicate truth values evolve under the concrete transition relation.

CEGAR (Counterexample-Guided Abstraction Refinement) iterates:

1. Abstract: build finite-state model from current predicates
2. Verify: check property on abstract model (k-induction)
3. If safe: done
4. If counterexample: check if realizable on concrete model
5. If real: return Unsafe
6. If spurious: extract new predicates from the infeasibility proof, refine

Structs

AbstractModel

Enums

AbstractionResult

Functions

abstract_model

Create an abstract model from initial state and predicates (legacy 2-arg API).

abstract_model_full

Create an abstract model with Cartesian predicate abstraction.

cegar_verify

CEGAR verification loop: abstract, check, refine.