Maintaining soundness in hybrid verification approaches for stateful models: A case study

Formal verification techniques such as model checking (MC) and theorem proving (TP) have found increasingly widespread use in the design of critical digital systems as a means to ensure their functional correctness. However, both MC and TP have their limitations. TP generally requires non-trivial human intervention, and MC is limited by the state explosion problem. The situation for MC is especially daunting for systems with large data components. In these cases, it is common to rely on a model abstraction to make MC feasible. Unfortunately, this may also add inaccuracies to the verification process, rendering it invalid. In this paper, we build upon current research and propose a hybrid verification approach that leverages the automation of MC and the logical soundness of TP to build a highly automated, high confidence verification system. We perform a preliminary investigation of the effectiveness of this method by verifying a random access memory (RAM) model. We also discuss how the lessons learned in this case study can be extended and implemented in a robust verification system to verify other similar systems.