Manipulating Proof Certificate Invariants in the Presence of Model Transformations

Trust in the outcomes of state-of-the-art hardware model checkers is more and more related to the availability of external certification tools, especially when the result is a "pass" verdict that cannot be simulated. This article addresses one of the major weaknesses of proof certifiers: the difficulty of exploiting a proof certificate obtained after the model was pre-processed with optimizations and transformations. Most proof engines provide a certificate in terms of an inductive invariant that could be easily certified by an external checker on the transformed model. On the other hand, proving the correctness of each model transformation is basically infeasible using an external independent tool. Recent works have followed the idea of post-processing both the model and the inductive invariant, by generating a witness model and a transformed invariant: the certifier then checks that the invariant holds on the witness model and that the witness model is consistent with the original one. We follow here the alternative path of fully lifting the invariant, back to the original model, with a two-fold target: 1) simplifying the task of the model checker, which is only required to output the final invariant and a log of the transformations done; 2) possibly reusing the invariant for other tasks on the model, such as logic synthesis optimizations and proofs of other properties. Specifically, we target the following transformations: temporal decomposition, phase abstraction and equivalence and constant propagation. As this process requires existential quantification operations, we show how to exploit Craig's interpolation to generate new inductive invariants. We also address scalability issues by applying a state-of-the-art SAT-based simplification procedure capable of reducing the size of the generated invariants when converted to NNF form. We experimentally demonstrate the effectiveness of this approach on a set of invariants derived from publicly available hardware model-checking benchmarks.