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.

Precision-preserving optimizations:

• cubes in increasing order
• do not update variables if command cannot change them
• cone of influence to reduce the number of predicates to consider
• syntactic construction of predicates
• caching of calls to theorem prover

Further approximations:

• bounding cube length to 3
• distributing approximation through logical operations

Finite state space for now.

Bounded model checking for finite diameter systems.

BDDs: http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

Heuristic refinement

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