Predicate abstraction techniques (first part)
See predicate abstraction papers.
Three aspects:
- abstraction
- model checking (finite state or pushdown system)
- counterexample-driven refinement
Today: abstraction
Abstraction
Main readings:
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
Examples.
Computation using wp. Weakest predicate abstraction of a given formula. 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
Approximations:
- bounding cube length to 3
- distributing approximation through logical operations