Methods for exploiting SAT solvers in unbounded model checking

Modern SAT solvers have proved highly successful in finding counterexamples to temporal properties of systems, using a method known as "bounded model checking". It is natural to ask whether these solvers can also be exploited for proving correctness. In fact, techniques do exist for proving properties using SAT solvers, but for the most part existing methods are either incomplete or have a low capacity relative to bounded model checking. Here we consider two new methods that exploit a SAT solver's ability to generate refutations in order to prove properties in an unbounded sense.