See predicate abstraction papers.

Three aspects:

• abstraction
• model checking (finite state or pushdown system)
• counterexample-driven refinement

Design space of abstractions:

• Cartesian product of abstractions for each predicate
• powerset with cartesian abstraction (ignores dependences in pre and post)
• powerset that takes into account the entire state (reduced product)
• focus (splitting, case analysis)
• best transformer in abstract domain

Computation using wp. Boolean programs. Bounding cube length.

Finite state space for now.

BDDs.

Bounded model checking for finite diameter systems.

Heuristic refinement

• expressions in branches
• adding weakest preconditions
• Craig's interpolation