Lifting Temporal Proofs through Abstractions

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 abstraction back into the original program domain. In this paper, we show how this can be done for general types of temporal properties, relative to both simulation and bisimulation relationships between the two programs. We then develop simplifications of the general 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.