Predicate abstraction techniques continued
See predicate abstraction papers.
Recall three aspects:
- 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)
- push down automata and context free grammars, checking emptiness of context-free grammars