Explicit-Symbolic Modeling for Formal Verification

Опубликовано 6 сентября 2016, 16:45

In this talk we present a model that combines explicit and symbolic representations in an explicit-symbolic model checking tool. 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 together 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 labelled 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.