Explicit-Symbolic Modelling for Formal Verification

We propose a model that combines explicit and symbolic representations in an explicit-symbolic formal verification model. Both explicit and symbolic models have been successfully used in the verification of finite state concurrent systems, such as complex sequential circuits and communication protocols. The proposed model aims to use explicit and symbolic techniques simultaneously to verify the same model and to make it possible to employ the most efficient technique to each aspect of the model. First, we formalize the explicit-symbolic model and show how it can be generated from a labeled state-transition system. Then, we apply those ideas to systems described in the Verimag Intermediate Format and present the main algorithms for integrating the underlying models.