Model checking is often performed by checking a transformed property on a suitable finite-state abstraction of the source program. Examples include abstractions resulting from symmetry reduction, data independence, and predicate abstraction. The two programs are linked by a structural relationship, such as simulation or bisimulation, guaranteeing that if the transformed property holds on the abstract program, the property holds on the original program. Recently, several algorithms have been developed to automatically generate a deductive proof of correctness from a model checker. A natural question, therefore, is how to 'lift' a deductive proof that is generated for an abstract program back into the original program domain. In this paper, we show how this can be done for general temporal properties, relative to several types of abstraction relationships between the two programs. We develop simplifications of the lifting scheme for common types of abstractions, such as predicate abstraction. We also show how one may generate easily checkable lifted proofs, which find use in applications such as proof-carrying code, and in the use of model checkers as decision procedures in theorem proving.
展开▼
