Predicate abstraction techniques continued

See predicate abstraction papers.

Recall three aspects:

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

Today we deal with the last two.

Reachability checking for finite state systems using BDDs

Checking for finite diameter systems

Reachability checking for pushdown systems (if time permits)

Counterexample-driven refinement

Main reading:

Heuristic refinement

  • expressions in branches
  • adding weakest preconditions

Craig's interpolation theorem

Lazy Abstraction with Interpolants