Abstract: We present a framework for certifying verification results and efficiently generating diagnostic information in the domain of equivalence checking, preorder checking, and model checking of finite-state system. The central idea is to use a generic data structure called `abstract proof structure''(APS) to abstractly encode the proof structure by which a checker reaches its result. APS carries checker-independent evidence for justifying verification result and provides the basis for a variety of `post-verification" analyses.

In this framework, checkers are enhanced with bookkeeping code to produce APSs as their results instead of simple "yes/no" answer. A wide range of existing checkers can be modified to produce APS without compromising their time and space complexities.

An immediate usage of APS is to certify verification result by checking the consistency of APS submitted by checker. The primary goal of this framework is to improve the efficiency and flexibility of diagnostic generation routines. We show that many diagnostic analyses can be preformed using APSs, including some traditional (e.g., counterexamples [CGMZ95] in model checking and HML formulas [HenMil85] for bisimulation) and novel (e.g., vacuity detection [BBER97]) diagnostic schema. We also show how winning strategies for property-checking games [Sti95] can be built from APS. The analysis routines based on APS enjoy independence from checkers; hence they can be easily modified and migrated from one checker to another. APS may also be used for evaluating the quality of verification process. In essence APSs help standardize the output of checkers, and analysis routines therefore can be created and executed independently, which has other interesting applications such as a client-server architectures for verification and generating proof-carrying code.