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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com