See predicate abstraction papers.

Three aspects:

• abstraction
• model checking (finite state or pushdown system)
• counterexample-driven refinement

Today: abstraction

Main readings:

• Construction of abstract state graphs with PVS
• Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format)
• Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213

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