Constructing and Reasoning about Abstractions and Refinements

Project members:

Shiva Nejati, Arie Gurfinkel, Marsha Chechik


Most realistic artifacts are too large to verify directly and need to be abstracted. Such abstractions should be constructed so that verification of the abstracted system allows us to say something about correctness of the original system.

Classical abstraction is sound only with respect to universally-quantified properties, e.g., if an invariant holds on an abstract system, it holds on the concrete one. If a reachability property holds on an abstract system, it is not clear whether it holds on the original one. If a universally-quantified property fails to hold, one can use counter-example based abstraction refinement to make the abstraction more precise so as to avoid the spurious counter-example.

3-valued abstraction preserves truth and falsity of arbitrary temporal logic properties. Of course, it is possible that the verification engine determines that the answer to the property is Maybe, at which point the verification is inconclusive and the abstraction needs to be refined.

There are many ways to compute 3-valued abstractions. One of them comes from abstract interpretation of programs, where a predicate p is determined to be True if it is true in the concretization of the system, False if it is false in the concretization, and Maybe if its value in the concrete system cannot be determined.

Current and Future Projects in This Area

Most relevant publications and related work:

Classical abstraction and refinement

3-valued Abstraction and Refinement

Classical and 3-valued model-checking

  Last updated: Sept. 3, 2003