Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
429300 | Journal of Algorithms | 2008 | 14 Pages |
Abstract
The evolution of SAT algorithms over the last decade has motivated the application of SAT to model checking, initially through the use of SAT in bounded model checking and, more recently, in unbounded model checking. This paper provides an overview of modern SAT algorithms, SAT-based bounded model checking and some of the most promising approaches for unbounded model checking, namely induction and interpolation. Moreover, the paper details a number of techniques that have proven effective in using SAT solvers in model checking.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics