Interpolation-sequence based model checking
- 1 November 2009
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
SAT-based model checking is the most widely used method for verifying industrial designs against their specification. This is due to its ability to handle designs with thousands of state elements and more. The main drawback of using SAT-based model checking is its orientation towards ¿bug-hunting¿ rather than full verification of a given specification. Previous works demonstrated how Unbounded Model Checking can be achieved using a SAT solver. In this work we present a novel SAT-based approach to full verification. The approach combines BMC with interpolation-sequence in order to imitate BDD-based Symbolic Model Checking. We demonstrate the usefulness of our method by applying it to industrial-size hardware designs from Intel. Our method compares favorably with McMillan's interpolation based model checking algorithm.Keywords
This publication has 4 references indexed in Scilit:
- An Analysis of SAT-Based Model Checking Techniques in an Industrial EnvironmentPublished by Springer Nature ,2005
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977
- Linear reasoning. A new form of the Herbrand-Gentzen theoremThe Journal of Symbolic Logic, 1957