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
Readings:
Checking for finite diameter systems
Reachability checking for pushdown systems (if time permits)
- push down automata and context free grammars, checking emptiness of context-free grammars
Counterexample-driven refinement
Main reading:
Heuristic refinement
- expressions in branches
- adding weakest preconditions
Craig's interpolation theorem
- Gallier Logic Book, Section 6.5