Exact Abstraction: An abstraction is exact (with respect to a property or a class of properties) if there is no loss of information due to abstraction. Exact abstractions are strongly property preserving. Under-approximations can be strongly preserving for properties if the removed behaviors do not influence the verification result. This is difficult to claim in practice when the under-approximation is generated by incomplete “coverage” of the program using a set of test cases or by an incomplete model-checking run. In this case, “coverage” is measured in terms of the program structure, which does not provide strong evidence to argue for preservation of many classes of properties. Typical model checking optimization techniques such as partial order and symmetry reductions (Clarke, Grumberg, and Peled 2000) are strongly preserving under-approximations.
Another relevant technique is program slicing (Corbett, Dwyer, and Hatcliff 2000). Slicing reduces the behaviors of a program by removing control points, variables, and data structures that are deemed irrelevant to checking a given property. Given a program and some statements of interest from the program, called the slicing criteria, a program slicer computes a reduced version of the program by removing program statements that do not affect the computation at the statements in the criterion. When checking a program against a property P, a slicing algorithm removes all the program statements that do not affect the satisfaction of P. Thus the property P holds on the reduced program if and only if it also holds on the original program (that is., slicing computes an exact abstraction). Program slicing is provided by analysis tools such as SPIN and Bandera.