Model Checking: From BDDs to Interpolation

摘要

In this paper we describe the development of model checking from BDD-based verification, through SAT-based bug finding, to Interpolation-based verification. Model checking is an automatic approach to formally verifying that a given system satisfies a given specification. BDD-based Symbolic Model Checking (SMC) was the first to enable model checking of real-life designs with a few hundreds of state elements. Currently, SAT-based model checking is the most widely used method for verifying industrial designs. This is due to its ability to handle designs with thousands of state elements and more. Its main drawback, however, is its orientation towards "bug-hunting" rather than full verification. In this paper we present two SAT-based approaches to full verification. The approaches combine BMC with interpolation or interpolation-sequence in order to compute an over-approximated set of the system's reachable states while checking that the specification is not violated. We compare the two methods both algorithmically and experimentally and conclude that they are incomparable.