Combining Theorem Proving and Model Checking for Verification of Concurrent Systems

An integration of deductive verification and model checking have been investigated in numerous works over the last decade. We refer to the approaches, where theorem proving was used to reduce verification problems to a form which allows to apply model checking directly. We present a translation procedure from finite state Reactive Logic (RL) specifications of concurrent systems into the SMV model checker. As RL specifications can use arbitrary data types we demonstrate an application of data abstraction using a specification of communication protocol as an example. This paper was motivated by the results achieved in the previous work on verification of medical guidelines by model checking. The basis for this work is an implementation of the symbolic execution proof strategy for concurrent systems in the theorem prover KIV