This is an old revision of the document!
Predicate abstraction techniques
See predicate abstraction papers.
Three aspects:
- abstraction
- model checking (finite state or pushdown system)
- counterexample-driven refinement
Abstraction
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