LARA

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