A lightweight integration of theorem proving and model checking for system verification
Weiqiang Kong, Kazuhiro Ogata, Tatsuyuki Seino, Kokichi Futatsugi · 2005
Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs" in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.